Radu Bacioiu, CSE 584, fall 1998. Assigned Readings – Requirements and Specifications

1. Roundtable Contributions

This collection of short articles presents the opinions of different formal methods experts about the present state of the integration of formal methods in the computer industry (both software and hardware).

• M.G. Hinchey and J.P. Bowen – The authors recognize that formal methods should be used sparingly "at the weakest links in the chain of development" and, I would add, at the critical links. The benefits of applying formal methods should be carefully weighed against its costs. The article expresses belief that the software engineering professionals working in the industry are not prepared to deal with the formalism involved and that an "outside expert in formal methods" working with a team of regular software engineers is a viable solution. Conclusion: formal methods are good in some cases, but they’re not a silver bullet.
• R.L. Glass – Author is concerned that the debate over formal methods has become a holy war. He urges practitioners and academics to come together to try and first define then come to a truthful conclusion about the costs, benefits and the overall state of the formal methods. Like the previous article, author’s belief is that formal methods have their merits but these merits shouldn’t be overestimated. The more concrete the goals of the formal methodists the better the chances for their voices to be heard.
• C.B. Jones – Calls for academics (represented by the author "a decade ago") and practitioners to find middle ground. Researchers should be less strict and allow a "light version" of formal methods, and on the other hand practitioners should strive to become proficient in the usage of these lightweight formal methods and be aware of their benefits.
• D. Jackson and J. Wing – Authors advocate that formal methods should try and achieve less lofty goals, focusing more on the immediate tasks at hand. They believe formal methods can be used efficiently – for instance in detecting bugs – but only if they’re "adapted" so that the cost of using the method isn’t prohibitive for the practitioner.
• A. Hall – Is also of the opinion that the debate has become a holy war. Old wisdom: Academia’s point of view: "Formal methods are essential in developing mission critical software." Industry’s point of view: "Using formal methods is too expensive." New wisdom (from the industry): Producing mission critical software is possible without using formal methods but it’s awfully expensive. Talks about the usage of formal methods "light" (pretty much as described by the previous authors) at Praxis. The main savings come from less extensive "conventional testing."
• D.L. Dill and J. Rushby – Article describes how the formalism has been embraced by the hardware industry more readily than the software industry. Main driving force: economics. An error in a hardware product is in general more costly than an error in a software program – unless the piece of software in question is a safety critical application. Moreover, authors consider that hardware is intrinsically better suited for formal analysis than software.
• C.M. Holloway and R.W. Butler – Article is critical of the tools available to support formal methods deployment in the industry. The tools in question are generally built in academic circles, exercised on "toy examples" and are not really ready for industrial prime time. "Prototype tools must be built, but no one should expect such tools to be used regularly within industry." The article also recognizes that engineers in the industry can’t afford to make the significant cost/time hit of perfecting these tools. In the meantime, researchers aren’t willing to take the hit either because it is probably more profitable to employ their resources for producing a few papers instead of an industrial grade formal method tool. Once again, it all seems to revolve around economics.
• P. Zave – Argues that (similar to other engineering professions) theoreticians and not engineers are the ones who should bridge the gap between academic research and industry.
• M.J. Lutz – Engineers shouldn’t handle complex mathematical concepts. They should be given tables and formulae. In a sense, (looking back at a previous paper) that’s probably what "Design Patterns" try to achieve.
• D.L. Parnas – Author is of the opinion that formal methods have still to be proven viable in the industry. There is work that needs to be done in taking formal methods and adapt them for usage by common software engineers. And more importantly, if economic viability is proven (mice trapped) engineers will probably embrace formalism with more ease.
• D. Gries – Deplores that people outside a relatively small formal methods research circle lack the training necessary to make use of this formalism. He calls for more emphasis on math and logic skills to be taught to future computer engineers and computer scientists.

I don’t know whether or not these articles were written as a result of a real or virtual round table – probably not – but it was encouraging to see that most authors more or less came to the same conclusions. Among them,

1. Formal methods should be prepared a little further (made more "lightweight") to achieve maximum benefit for the industry
2. Software professionals should be trained in how to use formal analysis and to think in the spirit of formal methods.
3. Formal methods should be used wisely, when economically viable (something the industry seems to be pretty good at)
4. Holy wars should end, zealots do more harm than good. Let’s all sit down and talk about it.

2. Deriving Specifications from Requirements: an Example – Michael Jackson and Pamela Zave

This paper emphasizes the distinction between Requirements (what we want a program to do) and Specifications (how exactly the program should behave). This distinction is not obvious in the other papers for this class (e.g. the title of another paper is "Requirements Specification for Process-Control Systems"), so I take it Jackson’s definitions should be restricted to his work. The author picks a simple (too simple?) example and walks the reader through the procedure of refining requirements into specifications. Various terms are very carefully defined – the machine, the environment, shared phenomena, control. As I was reading the paper I was wondering how such a strict formalism would scale to a more complex problem. In the form presented in this paper, it probably wouldn’t.

3. Requirements Specification for Process-Control Systems – N.G. Leveson, M.P.E. Heimdahl, H. Hildreth, J.D. Reese

The paper describes the process of applying a formal specification language to a safety critical avionics system. The industrial size of the project gives this study a lot of weight. The formal language used for the project was actually developed and refined in parallel with using it to define the requirements. One can ask whether some of the aspects particular to the TCAS system aren’t embedded in the final version of RSML and whether the resulting RSML is actually suited for any software project.

One of the primary goals of the specification language was to be easily understood by the specialists in the "problem being solved" rather than solely by the computer engineers developing the system. During the process of defining the language, the authors had to make some tradeoffs. For instance, choosing readability over writability was essential in order to facilitate the review of the specification. The language borrowed many concepts from a language called "statecharts" – unfortunately only superficially referenced in the paper. In the second half of the paper the authors dive into language and modeling details. The entire process is geared towards ensuring a readable presentation. There are methods used to simplify charts, subscripts are leveraged to indicate the nature of an identifier (variable, state, function, event) – somewhat similar to the "hungarian notation" developed by Charles Symoni.

However, there is trouble even in paradise. Even after RSML was employed for a long period of time to develop the system, due to the mere size and duration of the project there were things that authors wished were better. I quote:

"As has been discovered by most people attempting to maintain such systems, an audit trail of decisions and the reasons why decisions were made is absolutely essential. This was not done for TCAS over the 15 years of its development and those responsible for the system today are currently attempting to reconstruct decision making information from old memos and corporate memory." In other words, even after applying the rigor of the RSML formalism documentation for the product is still limping.

"Because the TCAS pseudocode specification had evolved over a period of more than 15 years, the current version contains more complexity than is necessary." – isn’t that what code aging is all about?

Authors blame the above imperfections on the fact that their formalism was not employed from the very start of the project. However, until there is proof that formal methods can cure the problems mentioned above one should remain skeptical. These problems are traps too well known to the developers of large, industrial size systems.

4. Formal Methods: State of the Art and Future Directions – E.M. Clarke, J.M. Wing et al

The authors present in this paper a condensed history of how formal methods were employed in various academic and/or industrial circles and the results of these projects. The paper starts by identifying some of the main obstacles that thwarted usage of formal methods in the software industry: obscure notations, non-scalable notations, lack of tools. The authors continue by reviewing how students of the field have tried to overcome these problems while writing formal specification languages and verification tools. A good example of a specification language is the TCAS paper. On the verification front, model checking seems to have gained more fans in the software industry than theorem proving since the goals of the formalism are more modest. Model checking probably also comes closer the good old-fashioned QA approach to test a class of scenarios and find bugs. Hardware engineers on the other hand embraced theorem proving because of the simpler models and the greater need for flawless safety-critical components.

The "Future Directions" section of the paper is a "to-do" list and suggestions for future research. Authors identify what has worked in the past and what hasn’t and try to come up with some guidelines that might be found useful by formal methods researchers.