Open Collections

A framework for multi-notation, model-oriented requirements analysis

University of British Columbia

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 formal-isation process were exposed. In both cases, we achieved the benefits of multiple notations for specification without sacrificing automation in analysis.

Thesis/Dissertation

application/pdf

2009-06-19

For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.

http://hdl.handle.net/2429/9479

Computer Science

University of British Columbia

UBCV

DSpace