When designing software requirements and specifications are almost always unpopular and rarely given enough thought even though it is one of the most important areas of design. The papers discussed below hope to change the negative perception regarding requirements and specifications, along with making an argument to the reader and the software industry in general for the use of formal methods when determining specifications.
Opening the discussion on requirements and specifications, Michael Jackson and Pamela Zave familiarize the reader with the concept through a simple example. Specifically, the authors make the reader familiar with certain terms regarding requirements and specifications, as well as to introduce the concept of "machine versus environment."
The authors begin by introducing vocabulary. A controlled system is a machine that interacts with its environment "to bring about or maintain relationships in that environment," while a machine is defined as the hardware or software to be developed. Bringing these two together, a requirement is something that states desired relationships in the environment that will be brought about (or maintained by) the machine. Derived from requirement, a specification "describes the behavior of the machine at its interface with the environment." The authors then introduce that program refinement is simply refining a specification to a program. Refinement, the authors claim, can only be complete when all references to inaccessible phenomena (either from the machine or the environment) have been removed, leaving a description of machine behavior. It is this idea of describing requirements and deriving specifications from them that are important to the authors, a notion they spend the majority of the paper on conveying through a small example.
The example is the control of a turnstile at the entry of a zoo. The task is to develop the controlling software to this turnstile. Designating the machine to be the small computer that runs the turnstile software and the environment to be the turnstile itself, the next step is to decide what environment interaction is of interest. Using designation sets (where each designation describes phenomena that occur in the environment) the authors note their importance in preventing uncertainty or misinterpretations about the requirements.
The paper then moves on to the concepts of environment and shared phenomena—phenomena shared by both the environment and the machine. The importance is in designating where control of shared phenomena resides—the machine or the environment. The authors also note that there are two types of environment descriptions—optative and indicative. Optative describes what properties of the environment our program would like to bring about or maintain, while indicative describes the effect the environment will have on the behavior of the machine.
After giving examples of shared phenomena and determining the requirements of their example the authors move on to determining specifications. To be a specification the authors propose three criteria: (a) any environment phenomena mentioned are shared with the machine, (b) any constrained requirements must be machine-controlled and (c) constraints are expressed in terms of preceding events or states in preceding intervals.
When compared to related work in the field the authors point out that their system is simpler because it does not introduce additional complexity when attempting to determine requirements. By giving careful consideration to environmental properties and following the guidelines put forth in their paper, the authors conclude that their method can be applied to almost any problem, large or small.
I have never placed much importance on the environmental phenomena that Jackson and Zave describe, instead concerning myself only with the immediate technical aspects of the task at hand. What intrigued me however was how considering the machine and the environment (as well as the shared events between them) can help combat confusion about what the requirements really are. All too often I have constructed programs that met my requirements but did not take into account the needs of those immediately outside a few others and myself. If nothing else, Jackson and Zave have introduced a way of thinking—specifically machine versus environment—that may help me reach a more general audience.
Continuing the discussion on requirements and specifications, Nancy Leveson et al. presents a new method for writing requirements for process-control systems. Through TCAS, an example used by the authors, they hope to convey to the reader RSML (requirement state machine language) as an alternative to aid in the design of formal procedures.
The first stages of software development have, the authors’ note, the fewest formal procedures to aid in analysis and design. While some validation techniques involve building prototypes or waiting until near completion to test the entire system, Leveson offers a different solution. Their approach involves the construction of one state (machine)-based model that includes all the information needed to describe all the components of the system as well as the interface between them—and no more. By having one model formal analysis of the system becomes feasible, as well as reducing difficulty when making changes to the system later on.
After some background into the TCAS project and a brief discussion of definitions and concepts used in RSML the authors describe some of the criteria used in their (and they argue that should apply in any) language. The first is that the language specifies black box "behavior of the software only and [not] internal design information." The second and third criterions are minimality and simplicity, to help prevent time being wasted in areas that are not used often. The fourth and most significant criterion is that the language used must be unambiguous and have an underlying mathematical foundation—in short powerful enough to have various analyses performed on it yet remain simple enough to be understood by non-computer science professionals.
The rest of the paper describes how RSML compares and contrasts to Statecharts (defined as finite state machines augmented with hierarchy, parallelism and modularity) when applied to the TCAS system. The authors conclude with an analysis of RSML’s ability. Because their implementation was picked up as the de-facto standard midway through design, the authors conclude that RSML was a success. More importantly, formal methods can be applied to large, complex systems and application experts who are not versed in computer science or mathematics can evaluate the specifications.
From my perspective while I find RSML intriguing and definitely agree that it has potential to make software design easier and less prone to devastating bugs later on, I would not use it in my profession for two reasons. The first is that RSML appears to have a huge initial cost. Now, over 1-2 year project this may not be an issue, but when you are an Internet based application with 4-6 month turnaround RSML, to me, does not justify itself. The second is that I would like to see RSML applied to a system closer to my work. In the pervious discussion of reverse engineering the strengths of those papers involved taking source code from real world applications and applying their techniques to them—I would find it beneficial to see something similar with RSML before adopting it.
Taking a different approach in the discussion of requirements and specifications, Edmund Clarke et al offer the reader an overview in the areas of specification and verification as well as numerous case studies on how these methods were applied. The authors also discuss future directions of formal methods as well as to provide some insight into how they can be more widely accepted.
In the past the use of formal methods was all but hopeless as they were too confusing and few people had the training to use them effectively on the job. Only recently, the authors note, have their been any promising developments in formal methods as the hardware and software industries are beginning to adopt them. The authors also give some brief definitions and properties behind formal methods, similar to the Jackson and Zave paper. The benefits of formal methods, the authors argue, is deeper insight into the workings of a given system, having an object that can be formally analyzed and helping to improve communication between developers, testers and customers.
After numerous case studies on the successful application of formal methods the authors discuss how they can be used in the process of verification—specifically model checking and theorem proving. Model checking involves the construction of a finite model of a given system and verifying that desired properties of that model are true. Theorem proving, on the other hand, is a technique where "both the system and its desired properties are expressed as [mathematical] formulas." To prove a desired property one starts with the axioms of the system and works from there. The main difference between these systems is that model checking provides results in a relatively short time while theorem checking can work on infinite state spaces—something model checking has difficulty with. The authors intertwine their discussion of these concepts with numerous case studies from each technique, showing their respective successes.
The focus of the paper then shifts to the future directions of formal methods. To aid in more widespread acceptance the authors’ list numerous criteria that they would like to see regarding the concepts behind formal methods as well as the supporting tools built for them. They also note that education in formal methods is lacking and stress incorporation of them in all levels of education, as well as encouraging researchers to increase collaboration and continue to reach out to the software industry. The authors conclude with the notion of continuing to support formal methods while making them accessible to non-experts, as well as raising the idea of creating a new career path for specialists in them.
I believe this is a good overview of formal methods as well as addressing some of the concepts they need to address in order to be widely used in industry—specifically the notions of early payback and integration. I would agree that more education earlier on needs to be provided in regard to formal methods, as I went my entire undergraduate education (as a dual computer science and mathematics major) and only remember a few days ever being devoted to their discussion. Having developers and testers at least have a working notion of the fundamentals behind formal methods would, I believe, make the software development process more manageable.
The last paper is not really a paper at all—instead it is a roundtable discussion concerning formal methods. While there are numerous individual contributors, all the authors can all be grouped into five sections: point-counterpoint, formal methods light, formal methods in practice, engineering mathematics, and finally education.
The first two papers are a point-counterpoint on the use of formal methods. Michael Hinchey et al takes the point, hoping to dispel some of the myths involved in their practice. Formal methods, Hinchey argues, is not a magic cure, nor is the cost involved in using them significant. As long as formal methods are not applied without consideration, as well as having continued support and educational and tool development, formal methods should help the software industry. Robert Glass, taking the counterpoint, believes that formal methods are useless until a larger problem is addressed—that academia and industry see software development as two entirely different methods. When this misunderstanding is finally cleared, Glass feels that the resulting outcome would be that formal methods are severely overvalued.
Formal methods light, lead by Cliff Jones and Daniel Jackson, argues for a lightweight approach to formal methods in order to make them more attractive to the software industry. While lacking the breadth of coverage provided by formal methods in their entirety, applying them when needed would save time and energy and still help to produce systems of higher quality. Taking the opposing view, numerous authors argue for the use of formal methods in full. While each paper highlights various positives about formal methods, there are some common themes that can be found amongst them. First and foremost, formal methods can, if applied right, be an inexpensive alternative to the more traditional process of testing software. To allow this however, there must be better supporting tools available to the industry. Another common theme is having researchers interact with and apply their work to real world problems in order to give some solid examples to industry about the success of formal methods.
The final two series of papers deal with mathematics and education with formal methods. Michael Lutz and David Parnas both argue that mathematics need to play a role in allowing formal methods to reach the masses, although the current notation needs to be improved. Both authors, alluding to earlier papers, argue that more relevant real world examples are needed for formal methods. Parnas continues on, stating that more time needs to be spent developing existing methods instead of searching for new ones. Concluding the roundtable, David Gries discusses some of the educational problems found with formal methods. Pointing out that formal methods are ignored in undergraduate courses, he cites fear of mathematics and the view of formal logic as simply an object of study as two main reasons. To combat this Gries argues for the teaching of logic as a useful tool to help change the attitudes of students and the industry towards mathematics and formal methods.
This roundtable provided a welcome change from the three more traditional papers. The two opinions I would agree with most are that of Glass and Parnas. I believe that the academic and industrial sides of software development each have widely different views of each other, and I think that more work needs to be done on improving exiting formal methods. I would like to see formal methods used more in my profession, but as this roundtable shows there is a lot of work to be done yet—on both sides.
The process of requirements and specification, while traditionally not popular, is one of the most important when designing software. To that end this series of papers have introduced to the reader the concept of formal methods and how they can make the process of requirements and specifications easier while adding value at the same time. While used in academia, formal methods have yet to make headway into industrial use, with the primary reason echoed by the authors being a lack of good examples of successful use of formal methods on an industrial system—an assessment I would agree with.