Evaluating FM

Today I read a couple of relatively short papers. The first one was Why Are Formal Methods Not Used More Widely?, by Knight, DeJong, Gibble, and Nakano. This paper is basically a study of whether or not there is anything to the popular notion that formal methods are not for real-world projects.

The study is divided into two parts. The first presents a sort of framework for evaluating the usefulnes of formal methods. There are several points around which the framework is stated, but the gist of it is that formal methods should complement existing development practices, rather than clashing or insisting on replacing them. And, of course, this goes for tools as well as practices. From this general idea, the authors derive a list of more concrete criteria for evaluating a formal method.

The second part of the paper is a case study of a control system for a research nuclear reactor at a university. The system was specified using three different formal methods: Z, Statecharts, and PVS. These formal specifications were then examined by a team of nuclear engineers and a team of computer scientists (who lacked extensive training in FM). The results were mixed, but the general consensus was that the formal specifications were certainly better and more reliable than the natural language ones previously used.

The second paper was short article form 1999 by Chechik and Wong entitled Formal Methods When Money is Tight. This one is about how to make formal methods useful for commercial projects, where short-term costs and development time are considered more important than product reliability. Basically, most of the points were related to making FM more accessible and easier to use, especially in terms of integrating with existing methods. The idea is to use formal methods in a way that allows tem to provide concrete, short-term benefits, as opposed ot nebulous reliability increates that are supposed ot eventually trickle down to reduced costs.

Another potential source of short-term cost savings is leveraging the strict semantics of formal description languages for automated development of test cases. The authors summarized a case study they did at Nortel that involved a tool that supported formal specification and test generation. Of course, not all methods provide that, but it certainly sounds nice.