Report on Assigned Reading3 - Requirements and specification

By - Anju Gupta

University of Washington, CSE584 – Software Engineering

11/16/98

In the software system development life cycle, the earlier stage, of collecting the correct requirement and deriving specifications from it is very important for constructing reliable systems. With the increase in complexity of the software systems these days the chances of introducing errors at this stage are getting greater. Formal methods are the techniques and tools, which can be used in specifying and verifying software systems for constructing more reliable systems.

Formal Methods: State of the Art and Future Directions by Edmund Clarke and Jeannette Wing

Specification is a process of writing down the description of the system and its desired properties so as to understand the system better uncover design flaws, inconsistencies, ambiguities and incompleteness. Verification can explain by two formal methods, model checking and theorem proving. Tremendous advances in the past decade has been made in the area of formal methods still further work needs to be done in the areas of: composition, decomposition, abstraction, reusable models and theories, combinations of mathematical theories and data structures and algorithms. The criteria which should be satisfied by the formal method tool to be attractive to practitioners are: early payback, incremental gain for incremental effort, multiple use, integrated use, ease of use, efficiency, ease of learning, orientation toward error detection, focused analysis and evolutionary development. No one formal method is likely to be suitable for describing and analyzing every aspect of a complex system, a practical approach is to use different methods in combination. Education is vital to the success of the formal methods.

I couldn’t agree more with Edmund and Jeannette remark that the specification is a useful communication device between customer and designer, between designer and implementers and between implementers and tester. For a report writing project I worked, which was called Rapid application development by a consultant on the project, who would sit next to the user and start coding after discussing the requirements. It costed this project a lot of money and human resources to fix this the problems due to the design flaws in the code, miscommunications between the whole development team as well as the end users.

Deriving Specifications from Requirements by Michael Jackson and Pamela Zave

With the help of a simple example this paper presents some elements of a methods for describing requirements and for deriving specifications from them. Two kinds of environment description is discussed for developing requirements, they are optative mood and indicative mood. The paper defines a requirement as desired relationships in the environment that will be brought about or maintained by the machine. Where as a specification describes the behavior of the machine at its interface with the environment. A specification is derived from a requirement. The derivation is made possible by environment properties that can be relied on regardless of the machine’s behavior, this is called refinement. The purpose of the refinement is to remove all non-executable elements from the specifications and to remove all references to inaccessible phenomena from the requirements. Reasoning based environment properties that can be relied on independently of the machine’s behavior bridges the gap between requirement and specification.

I found this paper very informative in defining the specification and requirements and their relationships. The example of the control of a turnstile at the entry to a zoo was simple to follow.

 Requirements Specification for Process-Control Systems by Nancy Leveson, Mats Heimdahl, Holly Hildreth and Jon Reese

This paper explains the importance of formal methods at the early part of development life cycle of the software project. It tries to prove its point by implementing a formal analysis procedure to the model, TCASII, a collision avoidance system. The goal is to ensure the software requirement model satisfies required system functional goals and constraints, including safety. With this implementation the paper describes not only the practicality of writing a formal requirements specifications for a complex, process-control system but also feasibility of building a formal model of a system using a specification language easily readable and reviewable. The difficulties were faced when applying forward and reverse engineering to the model. They were difficulty abstracting away from the design and difficulty deriving the requirement specification from the pseudocode.

I always like to build prototypes at the early part of the projects. Playing with the prototypes has always helped me identify the problems or design flaws which I would have missed by just reading the specifications documents. Prototypes have also help me understanding the new software technologies to decide on its pros and cons before moving further down the development path. Although I agree with Nacy, Mats, Holly and Jon that just developing prototypes are not the solution to identifying all the unknown problems or bugs. It was interesting to read the example presented by them on implementing formal analysis procedures which could rescue us from missing out on important issues at the early stages of development cycle and thus designing a more stable system.

This paper discusses the point/counterpoint on the viability of the formal methods in industrial practice. Michael Hinchey and Jonathan Bowen identify four main reasons, as the causes of industry’s reluctance to acceptance of formal methods are Misconceptions or Myths, Standards, Tools, Education and Training. In Robert Glass’s view, the reason for formal methods unacceptance is due to three main reasons: the formal methods is undefined, formal methods are under evaluated and lastly question whether formal methods are taking us in right direction. Cliff Jones with his twenty years of experience in formal methods, supports it, and explains why one should rigorously use the formal methods. Daniel Jackson and Jeannette Wing support the lightweight formal methods approach, which brings greater benefits at the reduced cost. The elements of lightweight formal methods are partiality in language, partiality in modeling, partiality in analysis and partiality in composition. Anothony Hall explains that no amount of argument will resolve the formal method debate unless the two sides, academics and industry, start to recognize each other’s objectives. David Dill and John Rushby explains some of the lessons learnt from the hardware design in acceptance of formal methods, they are: provide powerful tools, use verification to find bugs, formal technique must be targeted, researchers should apply their work to real problems. Micahel Holloway and Ricky Butler believe that the reasons of impediments to industrial use of formal methods are inadequate tools and inadequate examples. Pamela Zave, concludes the best way to use formal methods in an application domain is research, not development and the most effective thing to do is to bring formal methods into widespread use. Michael Lutz, outlines the differences between research mathematics and engineering mathematics and suggest some approaches that may accelerate the use of formal methods in industry. David Parnas, believes that mathematical methods will be the key to improved professionalism in software engineering. David Gries, explains the need for education in formal logic and hence changing the attitudes of practitioners toward mathematics, theory and formal methods.

I think the reason for the lack of use of formal methods in the software system development is due to lack of education about it. The goal of the education should not be only to make computer professional aware about it but in general I think the user community should also be taught about the advantages of it. This would generate of new breed of demanding users and the professionals would be forced to use and stop cutting costs. This paper was very informative. The discussion covered lots of points that were new to me.