Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results 
 
  Overview 
  Publications 
  Presentation 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

[This page is no longer being maintained. Please visit Nancy Day's Home Page at the Oregon Graduate Institute, Kendra Cooper's Home Page at the UBC Department of Electrical and Computer Engineering, and the resource page on Requirements at Intrepid Critical Software Inc. ]

Overview 
 
The formalWARE project focuses on the use of formal methods to address specific challenges in area of requirements specification and validation.  
   

Contents of this section include:

• Introduction to Requirements Specification and Validation 
• formalWARE Research on Requirements Specification and Validation  
• Standards and Certification Guidelines 
• Recommended Reading List 
• Recommended WEB Sites 

Introduction to Requirements Specification and Validation 

Requirement specification notations and validation techniques may be used to address the "better, faster, cheaper" objectives for describing the requirements for large or complex systems.  

Requirement Specification Notations  

Requirement specification notations may be categorized as informal (natural language), semi-formal (Structured Analysis), or formal (Z, statecharts, Petri nets). The use of formal specification techniques is increasingly popular, especially in Europe, as a method of improving the quality of a requirements specification. However, the usefulness of formal specification techniques is often limited by the fact that many conventional formal specification techniques are essentially mathematical shorthands which cannot be used effectively by domain experts without extensive training.  

When requirements are specified in natural language (e.g., informal English text), the potential for tool-assisted validation is limited to little more than common word processing functions such as "spellchecking". But when a formal specification technique is used, requirements are written in a formally defined syntax (just as other machine-parseable languages such as programming languages are generally based upon a formally defined syntax). Moreover, the use of a formal specification technique ensures that the requirements have a precise, unambiguous interpretation based upon an explicitly declared set of primitive concepts. Given a formally defined syntax and an unambiguous interpretation, the potential for tool-assisted validation of a requirements document is significantly increased beyond simple word processing functions.    

Validation Techniques  

Validation techniques are used to improve the quality of a requirements specification. A range of techniques is available, from simple parsing to mechanical theorem proving. The descriptions of the validation techniques below are from the thesis work in progress by Nancy Day on Formal Validation of System Specifications.  

Parsing and Typechecking. In order for a language to be machine-readable, it must have a well-defined syntax and therefore be parseable. While people would rarely take the step of defining a syntax for a language unless they are going to do something beyond just checking its syntax, it is beneficial to establish a limited vocabulary which can be used to communicate ideas. A well-defined syntax also creates a format that helps specifiers determine what information is needed.  

Once parsed, a typed specification may be typechecked. Typechecking is a mechanism for determining if constants are declared and used consistently in a document with respect to their types. This is an important step since it will catch simple errors such as spelling mistakes. If a modification is made in the specification, such as changing a name or type, type checking will catch all of the places in the specification affected by it.  

Together, parsing and type checking provide one way to determine if a requirement is "legal". If a requirement does not fit the syntax rules or does not typecheck, it should be rejected. This is analogous to the role a compiler plays in code development. Code with errors in it can be compiled, but the ``syntax errors'' produced by the compiler provide a first level of validation of the code.  

Completeness and Consistency Checking. A complete specification is one where all possible cases are covered in the specification. A consistent specification is one where none of the requirements conflict. Analysis for these properties could be done by manual review (i.e. require different outputs for the same input). For example, one form of completeness checking is checking that a total function is defined over all of its domain.  

Simulation and Prototyping. If a specification details a model of the system, it is useful to execute the model to create a simulation of the system being built. In simulation, the user can play the role of the environment of the system by generating events and stepping through the resulting behaviour of the system. This will not find all errors in the specification but it is a particularly effective means of communicating with a customer about the system that the specification is describing.  

One of the difficulties of simulation (just as in testing) is coming up with a reasonable set of simulation runs to try out the model and check its behaviour. Symbolic simulation is a way of executing the model using just symbols. For example, if our system does addition, we might want to name the values of the inputs to be x and y, and then look at the result which could be represented symbolically as x+y.  

In order to create a more natural interface to the system, it is possible to prototype a user interface for the system which is driven by the requirements specification. Many CASE tools include a facility for prototyping.  

Exhaustive Validation Techniques. Model checking is an automatic technique that tests whether a statement of the requirements of a system satisfies a given property. Usually the properties tested in model checking range over multiple states of the system. For example, safety invariants are properties that must always be true in a system.  

The properties must be stated in a well-defined formalism. Since it is useful to express properties that relate different instances in time, a temporal logic is often used. Computational Tree Logic developed by Clarke, Emerson, and Sistla (1988) is a branching time temporal logic that has been used for model checking.  

Model checking has been used extensively for hardware verification. It benefits from the efficient representation ordered binary decision diagrams, developed by Bryant (1986), provide for Boolean formula. A challenge in applying model checking to requirements specification is in dealing with specifications given at a high level of abstraction.  

Theorem Proving. Theorem provers have been used to support a variety of different approaches to requirements validation. They often require highly skilled experts and therefore do not become part of the toolkit of the average specifier. The amount of effort involved in their use also limits their effectiveness on large systems.  
   

formalWARE Research on Requirements Specification and Validation

Requirement Specification Notations  

Requirement specification notations addressed in the formalWARE project include the Structured Stimulus Response (SSR) in the thesis research of Kendra Cooper (UBC Electrical and Computer Engineering), statecharts and tabular notations in the thesis research of Nancy Day (UBC Computer Science), and value-passing CCS in the thesis research of Dilian Gurov (UVic Computer Science).  

The Ph.D thesis of Kendra Cooper focuses on tailoring established semi-formal specification techniques to be both formally defined and yet readable/writeable by domain experts. SSR is a textual approach to formal specification which allows requirements to be expressed in a form that looks very much like structured English, but which has a formally defined syntax and precise mathematical semantics.   

The readability of a formal specification may also be enhanced by the use of non-textual styles of specification which have been used previously by others to produce highly readable specifications. A major emphasis in the Ph.D. thesis research of Nancy Day is the integration of different styles of specification (e.g., statecharts, tables) into a common mathematical framework based on a typed, predicate logic called S.   

Please look at an example of a Statechart Specification.  

In related work, Nancy Day has prototyped a method of creating on-line specification documentation that integrates formal specification techniques with explanatory text, and includes features such as linking references to formal elements to their declaration or definition. The tool developed by Day includes the capability to automatically display certain kinds of definitions expressed in the S notation as tables.   

In addition to serving as input to validation tools, there is a potential to use the formal specification of a set of requirements as input to other tools which partially automate other requirements-driven processes. This illustrated in formalWARE by the Ph.D. thesis research of Michael Donat (UBC Computer Science) on the tool-assisted generation of test cases from formal specifications.   

Validation Techniques  

Parsing and Typechecking. Typechecking tools are being developed for the S notation and for the Structured Stimulus Response notation in the formalWARE project. For the S notation, the typechecking tool is called "Fuss". The use of Fuss to validate a formal specification written in S notation is analogous to the use of tools such as "Fuzz" to validate a formal specification written in Z notation. Fuss may be extended by users to incorporate user-defined analysis functions. A public domain release of Fuss and supporting documentation is in preparation. The typechecking tool for the Structured Stimulus Response notation is currently under development.  

Completeness and Consistency Checking. With her framework for integrating different styles of specification, Day has developed a means of doing completeness and consistency checking of tabular specifications. This work was illustrated by checking the completeness and consistency of a formal specification of the separation minima for the North Atlantic Region. This was a joint project carried out with Jeff Joyce (Raytheon) and Gerry Pelletier (Raytheon). The informal version of this specification had been thoroughly reviewed by a committee of ICAO (International Civil Aviation Organization). This analysis found two places unknown to the experts where the requirements are inconsistent.  

Please look at the "Separation Minima" specification.  

Simulation and Prototyping. A simulation or symbolic evaluation capability has been prototyped for two formal specification notations used in formalWARE.   

This includes the development of a simulator for statecharts by Nancy Day which has been used by RSC to simulate portions of an aeronautical telecommunications network. Among the more novel aspects of this simulator is the fact that the simulation algorithm is initialized directly by a machine-readable version of a formal semantics for statecharts given by Nancy Day in her M.Sc. thesis.   

More recently, Michael Donat has prototyped a symbolic evaluation tool for the S notation based on a form of logical deduction called rewriting. It is possible to write function definitions in S which looks very much like function definitions in a functional programming language such as Standard ML and then cause the application of these function definitions to be symbolically evaluated. One major advantage of symbolic evaluation of formal specification in this manner over the use of a conventional programming language for prototyping is that evaluation is done symbolically. This means that the uninterpreted primitives of the specification do not need to be instantiated minimizing the amount of "scaffolding" required to build an executable model.   

Exhaustive Validation Techniques. Other more specialized analysis functions are being investigated by both Nancy Day and Dilian Gurov in the area of "model checking". This allows a specification to be analyzed with respect to specific properties - for instance, whether it is possible for a concurrent system to reach an "impossible" combination of states. The "model-checking" technique can be a powerful alternative to simulation and testing for certain validation objectives. Similar techniques have already been used with considerable success to validate integrated circuit designs.   
 

formalWARE material on these topics: 

Publications:  

J.H. Andrews, N. A. Day and J. J. Joyce, Using a Formal Description Technique to Model Aspects of a Global Air Traffic Telecommunications Network. To be presented at FORTE/PSTV'97(1997 IFIP TC6/WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocal Specification, Testing, and Verification), Osaka, Japan, November 18-21, 1997.  

Nancy Day, Jeff Joyce and Gerry Pelletier. Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic Region: Complete Specifications and Analysis Results. Technical report 97-12, Department of Computer Science, UBC, October, 1997. 

Nancy Day, Jeff Joyce and Gerry Pelletier. Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic Region. Lfm 97: Fourth NASA Langley Formal Methods Workshop, Hampton Virgina, USA, September 10-12 1997.  

Jamie Andrews. Executing Formal Specifications by Translation to Higher Order Logic Programming. To be presented at the 1997 International Conference on Theorem Proving in Higher Order Logics, Bell Labs, Murray Hill, 19-22 August 1997.  

Jeffrey J. Joyce and Nancy Day and Michael R. Donat. S: A Machine Readable Specification Notation based on Higher Order Logic. In Lecture Notes in Computer Science 859, Higher Order Logic Theorem Proving and Its Applications, 7th International Workshop, (T.F. Melham, J. Camilleri Eds.), Springer-Verlag, 1994.  

Presentations:  

Specification and Tool-based Analysis of an Aircraft Separation Minima, Nancy Day, presented as part of the Lunchtime Learning Connection, Raytheon Systems Candad Ltd., Vancouver, 10 November 1997. 

Formal Validation of System Specifications, Nancy Day, presented at formalWARE's Open House, Vancouver, October 8, 1997. 

Formalization and Analysis of the Separation Minima for Aircraft in the North Atlantic Region, Nancy Day, presented at The Fourth NASA Langley Formal Methods Workshop, Hampton, Virginia, 10-12 September 1997.  

Formal Analysis of System Specifications, Nancy Day, presented at the Doctoral Consortium of the 19th International Conference on Software Engineering (ICSE), Boston, May 18, 1997.     

Standards and Certification Guidelines 

DOD-STD-2167A Defense System Software Development, Department of Defense, Washington, D.C., February, 1988.   

IEEE Std 830-1993 IEEE Recommended Practise for Software Requirements Specifications.   

Interim Defence Standard 00-55 The Procurement of Safety Critical Software in Defence Equipment Part 1: Requirements, Ministry of Defense, UK, April, 1991.   

Recommended Reading List 

D. Craigen, S. Gerhart, and T. Ralston, Formal Methods Reality Check: Industrial Usage, IEEE Transactions on Software Engineering , Issue 2 , February 1995, pp. 90-98.   

Alan M. Davis, Software Requirements: Objects, Functions and States. Prentice-Hall, Upper Saddle River, New Jersey, 1993.   

Tom DeMarco, Structured Analysis and System Specification, Yourdon Press, Englewood Cliffs, New Jersey, 1979.   

David Harel, On visual formalisms, Communications of the ACM, 31(5):514-530, May 1988.   

Michael Jackson, Software Requirements & Specifications: a lexicon of practice, principles and prejudices , Addison-Wesley, Wokingham, England, 1995.   

Robin Milner, Communication and Concurrency, Prentice Hall, New York, 1989.   

David Parnas and Paul Clements, A Rational Design Process: How and Why to Fake It, IEEE Transactions on Software Engineering , Vol. SE-12, No. 2, February 1986.   

James Rumbaugh, Michael Blaha, William Premerlani, Frederick Eddy, and William Lorensen, Object-Oriented Modeling and Design, Prentice Hall, 1991.   

J. M. Spivey, Understanding Z, Cambridge University Press, Cambridge, 1988.   

Paul Ward and Stephen Mellor, Structured development for real-time systems , Yourdon Press, USA, 1985.   

Jeannette M. Wing, A Specifier's Introduction to Formal Methods, Computer, 23(9):9-22, September 1990.   

Helene Wong, Informal, Semi-formal and Formal Approaches to the Specification of Software Requirements , M.Sc. thesis, The University of British Columbia, Department of Computer Science, 1994.   
    

Recommended WEB Sites

The Information and Archives site provides information and archives for the Software Requirements Engineering (SRE) mailing list.   

Formal Methods Specification and Analysis Guidebook for the Verification of Software and Computer Systems, Volume II: A Practitioner's Companion. NASA-GB-001-97 Release 1.0, May, 1997.   

This page has been accessed  times since November 27, 1998.