FM Thesis

Yesterday I muddled through chapter seven of Using Z. That was the chapter on relations. Mostly review, so there's not much to mention.

Today, I read through section nine of the IFM92 survey. This was the section discussing the formal methods used by the various projects and some of the possible areas for further research and development. It even included a hand breakdown of the projects and the methods, their uses, the tools involved, and things they needed. For purposes of this section, the exploratory cluster of projects were rolled into the other two, with TBACS going in with the regulatory cases and LaCoS and HP going in with the commercial.

There were a few general trends to note. First, the formal methods used tended toward those involving first-order logic and/or state machines. State machines were a bit more common in the regulatory cases, whereas Z dominated in the commercial cases. As previously noted, proof and refinement were more of a concern in the regulatory cases, but were largely unused in the commercial ones. It was also noted that the formal methods used were lacking in some areas, such as real-time and concurrency issues.

Another note of interest on the methods themselves was confusion over notation. Several projects had difficulty with non-FM experts being able to follow the notation. In some cases, graphical methods (diagrams, animations) were used to overcome this.

In terms of tools, they were lacking. Some projects used nothing at all, while most of the other projects used an incomplete toolset. The study authors generally concluded that improved support for automated deduction would have been a great boon to most projects. Also, a better selection of Z tools would have been helpful to the commercial cluster.

The last major point was regarding integration of FM with more conventional development methodologies. It seems obvious that this is a very important factor and that balkanizing formal and conventional methods leaves us with a sub-optimal process at best. The authors think that the SACEM and INMOS projects provide good examples of how FM can be integrated with the rest of the development process.