Thoughts on Requirements and Specifications

What is a requirement? How can we derive specifications from requirements? How can we refine a specification to make it executable? Jackson and Zave answered these questions in the paper "Deriving Specifications from Requirements: an Example".

A requirement is a desired relationship among phenomena of the environment of a system, to be brought about by the hardware/software machine that will be constructed and installed in the environment. A specification describes the behavior of the machine at its interface with the environment and should be sufficient to achieve the requirement. Specifications are derived from requirements by reasoning about the environment, using properties that hold independently of the behavior of the machine.

Although both of them are the connections between the real environment and the machine, this paper distinguishes requirements and specifications very clearly. The requirement is concerned entirely with the environment, while a specification is a restricted kind of requirement since it describes the behavior of the machine at its interface with the environment. Collecting requirements is relatively easy once we fully understand the environment and its properties. Deriving the specification from requirements is not that simple, though. On one hand, all the phenomena mentioned in the specification must be shared by the environment and the machine. On the other hand, the specification is a starting point for implementation. All the requirements in the specification should be able to be implemented technically. And the specification should provide detailed information, such as screen shot of user interface and exact hardware configuration requirement, for implementation. In some cases, specification has to compromise because of the implementation issues. So specification refinement is an important step during software development. In the industry, a specification document is usually written by the project manager. Then the development leads review the document to remove those non-executable elements.

The example presented here is a turnstile control system. It doesn’t include much user interfaces. Most projects I worked on are interactive systems between the user and the machine. User interface is a significant part of the spec. In order to come up with a user-friendly interface, we used an iterative process for some projects. We built a prototype and showed it to the potential users. We did some usability testing against the prototype. According to feedback from the user, we revised the specification and began to design the project. In this point, deriving specification is an iterative procedure. It involves human factor consideration, building prototype and usability testing. It helps us find mistakes in the specification and save some implementation time.

The paper "Requirement Specification for Process-Control Systems" concentrates on the earliest part of the methodology, requirements and specification, and demonstrates it on a real system. It describes an approach to writing requirements specifications for process-control systems, a specification language that supports this approach, and an example application of the approach and the language on an industrial aircraft collision advance system( TCAS II ). The approach is to model software blackbox behavior along with the assumptions about the behavior of the other components of the system, and then to apply formal analysis procedures to the model. The blackbox model separates the specification of requirements from design, simplifying the model and making the requirement model easier to construct, review and formally analyze.

This paper verifies that building a formal requirements model for a complex process control system is possible. More important, I think, it verifies that such a model can be understood and reviewable by non-computer scientists. One disadvantage for formal methods is that it is difficult for people without computer background to read. Formal methods are based on abstract logic and are some kind of mathematics languages. In order to be widely adopted in industry, easy to understand is a significant feature for formal methods.

With the growth of hardware and software system complexity, it becomes difficult to achieve reliability. Clarke presents some formal methods to solve this problem in the paper "Formal Methods: State of the Art and Future Directions". Formal methods are mathematically based languages, techniques, and tools for specifying and verifying complex systems. Many of these techniques are capable of handling industrial-sized examples. The process of specification is the act of writing thinks down precisely. Formal specification helps designers uncover design flaws, inconsistencies and gain a deeper understanding of the system being specified. There are two well-established approaches to verification: model checking and theorem proving. Industry is adopting these two techniques to complement the more traditional one of simulation for hardware verification. This paper finally suggests some general research directions that are likely to lead to technological advances.

One of the most important advantages for formal methods, I think, is that it saves the testing cost. Testing is a costly area, especially for large complex system. It is time-consuming to write down the test cases and very difficult or almost impossible to cover all the situations for the system. Formal specifications can generate test suites. Using model and proof-checking tools can determine formal relationships between specifications and test suites and between test suites and code. It will be a motivation for industry to use formal methods, especially for those safety-critical systems.

Since I didn’t use any of these formal methods before, I have no idea whether they are easy to use or not. Most of examples given are large software or hardware systems. I am wondering whether these formal methods can be easily applied to some medium commercial systems. As far as I know, some systems in industry are based on state transaction model. For instance, one project I worked on before is a finical application. Those major banks can use it to process checks and stubs, and save data to the database accordingly. This project is based on a state-transaction diagram. Each check and stub goes through certain steps sequentially. We used a state to indicate a step and defined the conditions from one step to another. When reading the paper, I think that some formal specification methods, such as Z and VDM, are suitable to the project. If these languages are easy to learn or if some powerful tools can be provided, more and more companies would like to use them for the specification.

This paper introduces many successful case studies. Actually I would rather to know more about the features of these formal methods. For instance, I would like to know the basic syntax of Z and how to apply it to the specification. Instead of enumerating all the methods and providing lots of examples, it would be better if it can pick up two or three typical methods and provides more information to the methods themselves. I don’t like this paper in this point.

Formal methods are well developed in the academic area, but they are not widely adopted in industry. The paper "Formal Methods: Point-Counterpoint" discusses a point/counterpoint on the viability of formal methods in industrial practice. Both researchers and practitioners discuss formal methods in different aspects: formal methods light, formal methods in practice, engineering mathematics and education.

Hinchey and Bowen identify the following four reasons for industry’s reluctance to take formal methods to heart: correcting the misconceptions, standards, tools and education and training. Robert Glass believes that there is a chasm that exists between software in academe and software in industry. It is pointless to try to address the advance of formal methods in industry until the broader problem of chasm is addressed. When I read these papers, I am wondering whether using formal methods will delay the development process and raise development cost. I think this is a common misconception in industry. It is good for Hinchey to point out that formal methods are not a panacea and formality should be used appropriately and judiciously at the weakest links in the chain of development.

But Cliff Jones is actually pleased with today’s level of awareness of more formal approaches to computer systems development. He suggests using a less-than-completely formal approach in most development cases. Jackson and Wing propose a lightweight approach, which in contrast emphasizes partiality and focused application, can bring greater benefits at reduced cost. They discuss partiality in language, in modeling, in analysis and in composition. Comparing research area, there are lots of more consideration in industry for market pressure, timing restriction and cost. I think that it is a critical requirement for industry to adopt formal methods: the benefit of formalization can be obtained immediately without massive investment. In this point, lightweight formal methods are pretty practical and useful. Actually it is a compromise result between researchers and software engineers.

Anthony Hall gives examples to proof that formal methods can make software development cheaper if used as part of an overall engineering approach. Dill and Rushby claim that formal methods are more successful in hardware design than software development. They believe the overriding reason is that applications of formal methods to hardware have become cost-effective. Holloway and Butler analyze the primary causes for the lack of wide-scale industrial use of formal methods: inadequate tools, inadequate examples, and the overlooking the gulf between the research world and the industrial world. By analysis of several software-modeling success cases, Pamela Zave draws the conclusion that finding the best way to use formal methods in an application domain is research not development. Powerful tools are very important for industry to adopt formal methods, I think. They will help engineers understand and use formal methods, and thus reduce the learning time and development cost.

Michael Lutz believes that the gap between researchers and industrial practitioners is largely due to a misunderstanding of the differences between research mathematics and engineering mathematics. David Gries emphasizes the need for education in useful formal logic. He thinks that logic underlies many formal methods and we should teach logic as a tool.

In one word, this is a very interesting paper. It provides readers different opinions from different points of view. There are a lot of argues about how to apply formal methods in industry. I knew nothing about formal methods before I took this course. None of the projects I worked on adopted such methods either. After reading these papers, I believe that more and more projects will use formal methods with their improvement. And most important, it is a great beginning for researchers and practitioners to sit down together and discuss about how to apply academic achievement to industry. This will benefit both sides.