Participating 
     Organizations 
  Research   
     Topics 
  People 
   

formalWARE 
    results  

  Overview 
  Publications 
  Presentations 
  Tools   
  Methods 
  Examples   
  Training 

formalWARE  
  information  

  Events 
  Index  
  Links   
  Contacts

This dissertation addresses the problem of how to bring the benefits of formal analysis to the changing world of multi-notation requirements specifications. We show that direct use of the formal operational semantics for notations in higher-order logic produces an extensible, systematic and rigorous approach to solving this problem. Our approach achieves the desired qualities without requiring theorem proving infrastructure. We concentrate on model-oriented notations that use uninterpreted constants to filter non-essential details. A key contribution is the de-coupling of notation from analysis technique.

We use type checking to regulate combinations of notations. Specifications are represented using embeddings that package the meaning of the notation with its syntax. We demonstrate our approach using combinations of the following three notations: statecharts, decision tables, and higher-order logic.

We introduce a new automatic technique called symbolic functional evaluation (SFE) to evaluate semantic functions outside of a theorem proving environment. SFE produces the meaning of a specification. Direct use of the semantics ensures that the same meaning for a specification is used by all types of analysis. SFE extends the technique of lazy evaluation to handle uninterpreted constants.

We focus on the binary decision diagram (BDD)-based analysis techniques of completeness and consistency checking of tables, simulation, and symbolic model checking. To bridge the gap between higher-order logic and automated analysis techniques, we create a toolkit of common techniques, such as Boolean abstraction.

We show that information contained in the structure of a specification can be used to supplement BDD-based analysis approaches by producing a more precise abstraction of the specification. The partition of a numeric value specified by entries in a row of a table provides information on how to encode numeric values in a BDD.

Our approach is demonstrated by the specification and analysis of two large real-world systems: a separation minima for aircraft and the Aeronautical Telecommunications Network (ATN). In the separation minima example, analysis discovered inconsistencies previously unknown to domain experts. In the ATN example, several errors in the formalisation process were exposed. In both cases, we achieved the benefits of multiple notations for specification without sacrificing automation in analysis.  

Download postscript  
Download PDF 

This dissertation is also available from Nancy Day's home page at the Oregon Graduate Institute (OGI). The individual chapters can be downloaded separately at that site.