FM Thesis

My reading today included an article that was recently linked on Slashdot of all places. The article was entitled Correctness by Construction: A Manifesto for High-Integrity Software and was written by Martin Croxford and Rod Chapman at Praxis HIS. It didn't contain too much I hadn't read before, but it did reference a couple of more recent projects. Other than that, it was just a general discussion of the "Correctness by Construction" method Praxis uses with some guidelines for use and statistics about their impressive productivity and defect rates.

I also slogged through another section of the 1992 International Formal Methods Survey (hereafter IFM92). This section was a summary of the results of the regulatory cases.

There were a few noteworthy things in this section. First, the emphasis of these projects was, unsurprisingly, on correctness and, in particular, the ability to offer proof of correctness, or, at least, to increase comprehensibility. In fact, the entire formal methods portion of the Darlington Nuclear Generator project was a post-hoc verification of an existing system in order to obtain certification.

Another interesting fact is that the regulatory cases were much more expensive than the other cases. In the case of Darlington, this is not surprising, as the entire FM effort was post-hoc and so could not reduce costs. What was surprising is that the price tag for FM at Darlington was $4,000,000, not lost profits for the certification delay. The SACEM project was also quite an effort, with the quoted statistic being 120,000 man-hours of effort.

Though the impact of FM on individual projects was good, the impact on the process/organization was mixed. GEC Alsthom subsequently used the methods developed for SACEM in other projects and the TCAS team received FM well. However the Darlington and MGS people were less enthusiastic and didn't display much interest in further pursuing FM.

A last tidbit was the use of tools. SACEM and MGS used tool support extensively, but Darlington and TCAS used none at all. The authors believe this is due to the relative immaturity of the methods used in those cases.

And as for maintenance of the software, the authors believe that FM will help, but did not have enough data to justify any conclusion.