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.
Z Tools
In an attempt to make one formal method, Z, more accessible I have developed a set of tools for writing and checking Z specifications in Microsoft Word.
My papers on formal methods
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.
I explain the different roles of formal methods at a Workshop on Industrial Strength Formal Methods. There is also a contribution to the debate about construction versus verification.
I have also published technical papers about how to use Z in object-oriented specifications.
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?”