Home

Seven Myths of Formal Methods Revisited

Software Engineering with Formal Methods: The Development of a Storm Surge Barrier Control System - Seven Myths of Formal Methods Revisited (2001), by Jan Tretmans, Klaas Wijbrans, Michel Chaudron:

Bos is the software system which controls and operates the storm surge barrier in the Nieuwe Waterweg near Rotterdam. It is a complex, safety-critical system of average size, which was developed by CMG Den Haag B.V., commissioned by Rijkswaterstaat (RWS) – the Dutch Ministry of Transport, Public Works and Water Management. It was completed in October 1998 on time and within budget.

CMG used formal methods in the development of the Bos software. This paper discusses the experiences obtained from their use. Some people claim that the use of formal methods helps in developing correct and reliable software, others claim that formal methods are useless and unworkable. Some of these claims have almost become myths. A number of these myths are described and discussed in a famous article: Seven Myths of Formal Methods [Hal90]. The experiences obtained from using formal methods for the development of Bos will be discussed on the basis of this article. We will discuss to what extent these myths are true for the Bos project.

The data for this survey were collected by means of interviews with software engineers working on the Bos project. These include the project manager, designers, implementers and testers, people who participated from the beginning in 1995 until the end in 1998 as well as engineers who only participated in the implementation phase, and engineers with and without previous, large-scale software engineering experience.

This paper concentrates on the experiences of the software engineers with formal methods. These experiences, placed in the context of the seven myths, are described in section 3. This paper does not discuss technical details about the particular formal methods used or the way they were used; see [Kar97, Kar98] for these aspects. Moreover, formal methods were only one technique used in the development of Bos. The overall engineering approach and the way different methods and techniques were combined to assure the required safetycritical quality, are described [WBG98, WB98]. Testing in Bos is described in more detail in [GWT98], while [CTW99] will give a more systematic analysis of the results of the interviews
with the developers.

Discussion of formal methods and verification has come up a few times here on LtU. In line with the recent discussions on the need for more empirical data in our field, this was an interesting case study on the use of formal methods. The seven myths of formal methods are reviewed in light of a real project:

  1. Myth 1: Formal methods can guarantee that software is perfect
  2. Myth 2: Formal methods are all about program proving
  3. Myth 3: Formal methods are only useful for safety-critical system
  4. Myth 4: Formal methods require highly trained mathematicians
  5. Myth 5: Formal methods increase the cost of developmen
  6. Myth 6: Formal methods are unacceptable to users
  7. Myth 7: Formal methods are not used on real, large-scale software
By naasking at 2011-12-27 16:19 | Implementation | Software Engineering | Theory | other blogs | 25257 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Date of paper?

Out of curiousity, what does anybody have a date for when this paper was written? Judging from the bibliography, I'd say it probably was 1999 or 2000.

By Leon P Smith at Wed, 2011-12-28 00:27 | login or register to post comments

According to Citeseer, it is

According to Citeseer, it is 2001. Generally, I try to write down where the paper was published, if applicable. This one was published in Formal Methods of System Design (September 2001).

By Sean McDirmid at Wed, 2011-12-28 00:58 | login or register to post comments

Good point, I've updated the

Good point, I've updated the link to point to citeseer and added the date.

By naasking at Wed, 2011-12-28 01:42 | login or register to post comments

tangential remarks

A paper on formal methods coming out of the Netherlands? It reminded me of a much earlier paper of similar extraction: In Defense of Program Testing or Correctness Proofs Considered Harmful by Andrew S. Tanenbaum, ACM SIGPLAN Notices, Volume 11 Issue 5, May 1976. A delightful piece of English prose, and only five pages long at that. Do read it if you can get a hold of it. And if you can't, rest assured that it says pretty much exactly what you'd expect any reasonable person to say. (Too bad there don't seem to be any freely accessible copies floating around.)

And of the sake of archival completeness, let me also note that the original “Seven Myths” paper (as well as its companion paper “Seven More Myths”) appears to have been mentioned here in passing in the distant past.

By el-vadimo at Wed, 2011-12-28 19:56 | login or register to post comments

Downloadable version of Tanenbaum's paper

From the digital repository of the Vrije Universiteit Amsterdam: http://dare.ubvu.vu.nl/handle/1871/2633

By alceste at Tue, 2012-01-03 15:24 | login or register to post comments

highly trained mathematicians

on the contrary, highly trained mathematicians can be a burden for a formal methods project. [...] we have had mathematicians involved who were searching for the shortest expressions in Z to express particular solutions, but these solutions were so short and tricky that nobody else [...] could read them.

This comment resonated with me. On the job in a C++ shop, I'm the "highly trained mathematician" who has to guard himself against inventing template-based designs that are difficult for others to work with. For my hobby coding in Haskell, on the other hand, I'm regularly stretched to understand which new, mathematically-inspired methods would apply to a project.

My impression is that mathematicians are less likely to be a burden in a Haskell environment than in the context described in the paper. I suppose some would get carried away with the abstractions and have a detrimental impact. However, if I were working in a Haskell shop I would hope that the top engineer had studied category theory, and that my fellow developers did not mind dealing with functors and monad transformers.

By Scott Turner at Thu, 2011-12-29 18:52 | login or register to post comments