Weaving formal methods into the software engineering mainstream, this paper summarizes three keynote speeches from the fifth Institute of Electrical and Electronics Engineers (IEEE) International Conference on Software Engineering and Formal Methods. The three speeches, given by Michael A. Jackson, Patrick Cousot, and Byron Cook, focus on the state of the practice in formal methods, and its relation and widespread adoption in the practical software engineer’s tool belt. The authors argue that the data and computational complexity of modern distributed software systems infect nearly every area of modern life, from routine household tasks, such as cooking food, to identifying the location of our vehicles while we drive, via global positioning system (GPS). The authors argue that software reliability theory is nearly as mature as that for hardware, and they offer suggestions for where the former should be going.

First, Jackson argues for the specialization of software engineers within a particular discipline domain (for example, automotive, aerospace, or safety-critical systems), leading to the domain’s “normal” design--the understanding of the best practices and approximative properties of successful systems within the domain, which are repeatable by other software engineers constructing systems within the domain. Jackson likens this to W.G. Vincenti’s definition of normal design discipline within aeronautics, comparing these phenomena to the striking similarity of automobiles in a particular product line due to their own normal design. Jackson also argues that while the normal design within a particular software engineering domain is what we should be striving for, “radical” design--the exploration of the problem and solution space for a particular family of software systems within a domain, similar to Greenfield Design--is also necessary, although predictably less reliable than systems built from a normal design.

Cousot’s contribution defines the notion of abstract interpretation in formal methods, demonstrating the need to approximate formal mathematical solutions to software reliability measurements. This is mainly due to the intractable nature of modeling a software system’s reaction with the outside world and outside inputs. The solution, according to Cousot, is to use abstract interpretation, the process of coupling an over-approximation of the underlying properties and states of the system with that of a sound under-approximation of the particular system reliability property to be proven. This research track has led to recent advances in static-analysis verification--the construction of a model from existing source-code relationships, without taking into account the system’s dynamic behavior--that in turn have been widely adopted in software engineering practice, since modern static-analysis tools work with the developers, instead of against them.

Finally, Cook focuses on the difficult problem of verifying properties in concurrent systems. Some of the main limitations of topical concurrent reliability assessment techniques (for example, modeling the occurrence of multiple simultaneous events and modeling the synchronization between processes) are dismissed by modern advances that focus on thread modularity. These advances reduce the complexity of assessing reliability by casting the problem as a collection of sequential software reliability verifications. Cook mentions that, while promising, the difficult part in thread-modularity techniques is finding the right set of sequential abstractions for a given program that will require the development of appropriate heuristics.

Overall, this is an informative paper that assesses the current intersection of software engineering and reliability measurement. The paper’s main drawback is the lack of detail on any one technique; this leaves readers scratching their heads on a few of the reliability assessment technique descriptions, as they are covered, admittedly, quite broadly rather than in depth. This being said, the paper is a short, worthwhile read, as it will bring any reader interested in the state of software reliability measurement and its future up to speed on the current state of the practice.