The role of formal methods
 A key idea of Correctness by Construction is that all stages of development should be as rigorous as practical. Formal Methods are the key to achieving this rigour. They allow you to
- Describe exactly what you want the software to do
- Check that your description is consistent and complete
- Describe critical safety, security or other properties and check that your software will satisfy them
- Describe the software design precisely
- Check that the design is consistent and will satisfy your requirements.
Practical experience
When used as part of a well-defined process such as Correctness by Construction. formal methods achieve very low defect rates and excellent productivity.
One example is the Multos CA project which was described in a paper in IEEE Software. I gave a more detailed account of the formal methods we used in a talk at FME’02. I described some technical aspects of the use of Z at Formal Aspects of Security.
A much earlier project, CDIS, was described in IEEE Software and an independent assessment of the effect of formal methods was published in IEEE Computer.
The effective use of formal proof on a safety-critical development was described in a paper in Transactions on Software Engineering.
My technical papers
I explain the different roles of formal methods at a Workshop on Industrial Strength Formal Methods.
Formal Methods have always been controversial. Seven Myths of Formal Methods was an early and much cited contribution to the debate. Still, not everyone is convinced: many people still ask “What have formal methods ever done for us?”.
I have also published technical papers about how to use Z in object-oriented specifications.
Other experience reports
There are two collections of industrial experience reports by Bowen and Hinchey.
Other sources of information
The world wide web virtual library contains lots of pointers to formal methods of all sorts.
Formal Methods Europe is the most active organisation for those interested in formal methods application or research.
The Formal Techniques Industry Association has recently been formed to promote the use of formal methods in industry.
|
