Home Page
methods
last updated November 27, 1998 
 
 formalWARE 
    project  

  Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results 
 
  Overview 
  Publications 
  Presentation 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

Overview

formalWARE researchers developed a number of methods as part of their project related research. This page focuses mainly on methods which may be used without tool support. Other methods more closely associated with tools are described by the user manuals for these tools and associated documentation.

Contents of this section include:

Stimulus Response Style Requirements Specification   

This is a method of specifying requirements in a style which is strongly motivated by a method developed by Hughes Aircraft of Canada Limited (now Raytheon) to specify the software requirements for the Canadian Automated Air Traffic System (CAATS). The specification of requirements in terms of externally visible stimuli and responses is a core concept of this method. Although it bears some similarities with "Uses Cases" and scenario based approaches to requirements specification, many of the core concepts of this method can be traced back to test methodologies from the 1970's. Kendra Cooper's formalWARE research will yield a fully documented method of specifying requirements in this particular style.A forthcoming Technical Report by Cooper et al. may be used as the basis of a "guidebook" for the specification of the requirements of a system using this method. Cooper is also developing extensions of this basic method that will allow a variable degree of formalization (i.e., formal syntax with a formally defined semantics) to be used on a selective basis within a requirements specification document based on this method. She is also developing prototype analysis tools for this method, but the method can be used without the tools. More information on this method may be found in: 

Refinement of Hazards into Safety Verification Conditions   

This is a method for the discovery of safety verification conditions from the definition of a hazard. The method can be carried out to various depths. When the method is carried out to the level of a black box view of the system, the result is a set of system safety requirements. The method has similarities with Fault Tree Analysis (FTA) and Software Fault Tree Analysis (SFTA). Like FTA, a given hazard is traced backwards through the system to cover all the ways in which a hazardous condition can occur. Like SFTA, a "proof-by-contradiction" style reasoning is employed. This method is a result of research by Ken Wong on software safety verification. 

Tabular Specification of Decision Logic   

This is a method of using tables to specify decision logic. It is based on a particular style of tabular specification developed by Nancy Day as a refinement of the well established concept of "AND-OR" tables. A tool called Fusion, also developed by Day, may be used to analyze decision logic represented in this tabular style for completeness and consistency. To facilitate analysis of the specification by Fusion, the text within the tables must be expressed in a variant of S called S+. The main illustration of this approach is based on the formal specification of an aircraft separation minima. This tabular style of specification may also be used (without tool support) in a semi-formal manner where English may be used as text within the tables rather than S+ expressions. More information on this method may be found in: 

Requirements-based Testing  

A method for the requirements-based testing of a system should normally include guidance on the amount of detail that must be provided in the specification of individual test cases. The method should also provide guidance in decomposing logically complex requirements into test cases. Work by Michael Donat on the automation of processes used to generate test cases from requirements has resulted in a variety of techniques and concepts which can be regarded as elements of a method for requirements-based testing. For instance, Donat's work distinguishes between "base style" and "differentiated style" specification of "test frames". This distinction provides a basis for determining the amount of detail that should be provided in the specification of individual steps of a test procedure. Donat's work also provides objective definitions of several different kinds of coverage criteria for requirements-based testing. These definitions of different coverage criteria may be used within a manual approach to provide guidance in the development of a test procedure. They may also be used as a basis for the assessment of the "completeness" of a test procedure with respect to a set of requirements. 

Organization and Content of a Safety Verification Case  

An important step in the overall safety engineering process is the verification of the source code with respect to the hazards. As discussed in chapter 18 of Nancy Levenson's seminal textbook on software safety, Safeware, this step is necessary even after system hazards have been identified and controlled through design, to determine if any mistakes were made in the safety engineering process. In general, there is a need for more effective methods for the safety verification of the source code. In particular, there is a need for methods that will deal with large software-intensive systems with modern architectures. Static code analysis techniques, such as software fault tree analysis, have mostly been applied to relatively small systems.

Ken Wong's M.Sc. research involved the development of a practical, comprehensive process for constructing a safety verification case for the source code. The safety verification case is intended to provide a rigorous, repeatable and recorded argument that the hazard cannot occur given specific, explicitly stated assumptions about the hardware and software.  

Other Methods  

Several additional method will eventually be described here (as results of the formalWARE project).  These will include:      

    Statecharts-style specification in a textual form 

    Development of Safe Software Components