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).
I dont 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,
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 Jacksons 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 wouldnt.
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 arent 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." isnt 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 hasnt and try to come up with some guidelines that might be found useful by formal methods researchers.