Should I use formal methods on my software project?

Question

Our client wants us to build a web-based, rich internet application for gathering software requirements. Basically it's a web-based case tool that follows a specific process for getting requirements from stakeholders. I'm the project manager and we're still in the early phases of the project.

I've been thinking about using formal methods to help clarify the requirements for the tool for both my client and the developers. By formal methods I mean some form of modeling, possibly something mathematically-based. Some of the things I've read about and are considering include Z (http://en.wikipedia.org/wiki/Z_notation), state machines, UML 2.0 (possibly with extensions such as OCL), Petri nets, and some coding-level stuff like contracts and pre and post conditions. Is there anything else I should consider?

The developers are experienced but depending on the formalism used they may have to learn some math.

I'm trying to determine whether it's worth while for me to use formal methods on this project and if so, to what extent. I know "it depends" so the most helpful answers for me is a yes/no and supporting arguments.

Would you use formal methods if you were on this project?

Answer 1

The true question to ask here is not whether to use them or not, but what is gained and lost.

Will the productivity and outcome outweigh the complexity and learning needed?

Answer 2

In general you should use what the team is comfortable with. With new items there is going to be a learning curve, which means there are going to be questions about the process and mistakes made. Part of your development timeline will be used to correct these problems, and if you aren't planning on using them with this team in the future, really you're not going to have a long term gain by introducing something new. Change process takes a long time and a lot of work.

If you have estimated enough time to handle these problems you might be ok.....if your estimation is correct. Considering that you haven't worked with these people (at least that is what your post sounds like), chances are your timeline isn't going to be as accurate as it should which mean you could have not allocated enough time to finish the project let alone introducing a new process.

The other question you have to ask your self is "how comfortable are you with the process you want to implement?" I never try and introduce a new process on a project unless I know that I can pull the team through it if I have to. Trying new things from time to time is good, but you need to have a team you are comfortable with to know how to navigate out of a tight situation.

Answer 3

I've been thinking about using formal methods to help clarify the requirements for the tool for both my client and the developers.

Very few developers have formal methods experience. The only time I've seen clients with formal methods training were members of the ZUG when we were porting CADiZ to Windows.

By formal methods I mean some form of modeling, possibly something mathematically-based. Some of the things I've read about and are considering include Z (http://en.wikipedia.org/wiki/Z_notation), state machines, UML 2.0 (possibly with extensions such as OCL), Petri nets, and some coding-level stuff like contracts and pre and post conditions. Is there anything else I should consider?

There's a very large gap between Z, which is a formal method, taking its basis in set theory, and UML, which is a informal notation with some semi-formal notations (state machines) tagged on.

Some technical clients, such as you'd expect to find using a software requirements tool, are quite comfortable with UML.

There may be value creating a Z model of your domain, and there may be value in creating a pi-calculus model of your messaging between client and server (or petri-net, but I find pi is both simpler and more powerful).

What a Z model of your domain would give is an implementation independent set of type constraints, expressed more powerfully than the type system of any common implementation language.

What a formal model of your messaging would give you is the facility to run analyses to ensure you don't lose updates or get conflicts or deadlocks.

What a UML model gives you is a notation for breaking a large system up into function areas (package diagrams), of showing how classes in those areas relate to each other statically (class diagrams), of showing how instances of those classes relate dynamically (sequence, activity and interaction diagrams), and showing how the packages are deployed (component and deployment diagrams). These are useful for communication in the team, and to get ideas fleshed out a bit, but don't have formally defined semantics which allows very sophisticated analysis.

The Z specialists I worked with in the '90s considered the idea of specifying a CASE GUI in Z ridiculous. Creating a UML model for such a GUI is commonplace.

I haven't used formal design-by-contract pre and post conditions, though I do sometimes add them in comments, and frequently in assertions, and I unit test conditions which might violate them.

Answer 4

I agree totally with Tom and ask the same question,

Will the productivity and outcome outweigh the complexity and learning needed?

In my opinion unless the system/software can be identified as “safety-critical” formal methods are unnecessary.

What safety-critical mean:

When the failure of a computer system can lead to catastrophic consequences, such as the loss of human life, damage to the environment, or damage to the system itself, such a system is known as “safety-critical”.

Answer 5

I agree with both Tom and Abufardeh - Will the productivity and outcome outweigh the complexity and learning needed?

Also, is this methd better for getting ALL the requirements before development (amd ensuring these requirements are both well-defined and testable)? Getting all the requirments first seems like common sense, but a large percentage of programs do things in parallel thinking it's no problem to get some requirements later. Requirements creep is a nightmare! The movie "The Pentagon Wars" is an eye-opener to anybody who disagrees.

Answer 6

I've been looking at several approaches to 'lightweight' formal methods, for applications that may be mission-critical, but not life/safety critical. Some ideas:

• Alloy
• SysML
• SPIN
• Others???

Answer 7

Late in the game here but you might consider something like testable architecture through Savara which we use for many projects where there is a predominance of communication or interaction between components. This is most often seen in any SOA backend to a web frontend.

It is formally grounded in pi-calculus and you don't need to understand pi-calculus to use it.

Cheers

Steve T