Formal Methodologies: Build it and they will come

This lecture will introduce some examples of formal methodologies; formal software design methods do not recognize any distinction between software and programs. By removing any distinction between software and programs, the formal strand seeks to introduce mathematical rigour into both program and software design.

This lecture is also the first lecture in where you will be expected to produce a seminar paper in time for the scheduled seminar session next week.

Formal Methods - a summary

From a philosophical viewpoint, formal methods adopt a realist ontology and rationalist epistemology, that is they assume there is a correct answer to any particular problem and that this can be discovered by the application of logic and reason. They treat software and program descriptions as though they were equivalent; assuming both to be complete and closed descriptions of an underling reality. Making this assumption creates a seamless equivalence between the software (program) description, the representation in the designers mind and the underlying aspects of reality that are being modelled.

Formal Methods - pros and cons

Pros

Software design methods in the formal strand reason about software and programs using the same tools and techniques. This should mean that software and program design can be brought together to streamline the design process as a whole and, as these tools are built on logic, increase the designers confidence in the accuracy of the final design. Program design methods can usually assume the description is closed, however, software design methods must deal with partly open descriptions, which can be a significant problem for methods in the formal strand.

Cons

Formal methods provide a set of tools for reasoning about a description, but offer little assistance in actually arriving at that description. Consequently, designers often find it difficult to apply these methods as they give them little assistance in working with anything other than complete and closed descriptions. Some argue that this is in fact an advantage because it prevents 'fuzzy thinking'; some go as far as to claim that the principal benefit of using formal methods is that they focus the designer's attention on the problem of validation.

Reading

Books

• See any of the books from the SDM books section

Articles

• Chapters 5 and 7 in D . Avison and G Fitzgerald, Information Systems Development: Methodologies, Techniques and Tools (3rd Edition), McGraw-Hill Publishing, 2002
• Hall, A. (1990). Seven Myths of Formal Methods. IEEE Softw., 7(5), 11-19.
• Bowen, J. P. and Hinchey, M. G. (1994). Seven More Myths of Formal Methods, Proceedings FME'94 Symposium:Springer-Verlag LNCS.
• Bowen, J.P. and Hinchey, M.G. (1995). Ten Commandments of Formal Methods, Computer, vol. 28, no.4, pp. 56-63, April, 1995.
• Tretmans, J. Wijbrans K and Chaudron, M. (2001). Software Engineering with Formal Methods: The Development of a Storm Surge Barrier Control System Revisiting Seven Myths of Formal Methods, Formal Methods in System Design, Volume 19, Number 2, Date: September 2001, Pages: 195 - 215

On-line Articles

• Why Are Formal Methods Not Used More Widely? John C. Knight, Colleen L. DeJong, Matthew S. Gibble, and Luis G. Nakano. (1997) in: The Fourth NASA Langley Formal Methods Workshop (Lfm97), pages 1-12, September. NASA Conference Publication 3356
  This paper addresses the issue of why formal methods not more widely used. The approach taken to answering this question was to develop a formal specification for a safety-critical application (a nuclear reactor) using different specification notations (Z, PVS and state charts) and then have the results assessed by (a) the developers themselves, (b) a group of engineers (c) a group of computer scientists.

• Formal methods and testing: why the state-of-the art is not the state-of-the practice. Rosenblum, D. S. (1996). SIGSOFT Software. Eng. Notes, 21(4), 64-66.
  This paper is a short 3 page summary of a workshop in formal methods, it provides some interesting insights into the reasons why the formal method community think that formal methods are not more widely used.

• From formal models to formally based methods: an industrial experience. Ciapessoni, E., Mirandola, P., Coen-Porisini, A., Mandrioli, D., and Morzenti, A. (1999). ACM Trans. Softw. Eng. Methodol., 8(1), 79-113.
  A technically oriented paper that examines the reasons why formal methods have not been more widely accepted in industry and addresses the assertion that 'The problem with Formal Methods is that they are just formal, not methods' by describing how the TRIO specification language could be used throughout the systems development process.

• Observations on industrial practice using formal method. Gerhart, S., Craigen, D., and Ralston, T. (1993). Baltimore, Maryland, United States: IEEE Computer Society Press.
  This paper presents the results of a systematic survey of the use of formal methods in industry. Two cases are examined and three key questions addressed: 'On what kinds of applications have formal methods been used?', 'What kind of organizational needs lead to the use of formal methods?' and 'What results were achieved?'

A practical example

• An experience in the formal verification of industrial software. Staskauskas, M. G. (1996). Communications. ACM, 39(12es), 256.
  This paper is a personal account of applying formal methods (UNITY) to an industrial problem (the design of an input / output subsystem in a concurrent operating system). The UNITY methodology is described briefly and the application of the methodology to the problem is described in more detail. The final section of the paper contains a discussion of the pros and cons of UNITY in this particular application together with some recommendations of how things could have been improved.

Web pages

• Formal methods - a collection resources related to formal methods from the web site 'Online Computer Science Degree'.
• Formal methods - this is the top level in the category "Formal methods" from Wikipedia.
• Index of Resources - Index of Resources for Z maintained by Ian Toyn.
• Information on the Vienna Development Method - From The VDM Portal maintained by John Fitzgerald

Lecture notes

The notes for this session are available as a presentation (in pdf format) - lecture notes for session 4