A Framework for Multi-Notation, Model-Oriented Requirements Analysis
Nancy A. Day
Ph.D. Thesis.
Department of Computer Science, UBC, October, 1998.
Abstract
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.
Bibtex Entry
@PHDTHESIS{DayPhd98,
AUTHOR = {Nancy Ann Day},
TITLE = {A Framework for Multi-Notation, Model-Oriented Requirements Analysis},
SCHOOL = {Department of Computer Science, University of British Columbia},
YEAR = {1998}
}
Related tools
I will soon be making the tools I implemented to support my thesis
work available on-line.
Download
My thesis is very long (424 pages). I've broken it up into parts so
you can either download the whole document or just the chapters of interest.
All of these files are gzipped postscript.
Download whole thesis (528 K)
Title page and table of contents (61 K)
Acknowledgements and dedication (53 K)
Chapter One: Introduction (80 K)
Chapter Two: Related Work (73 K)
Chapter Three: Foundations (66 K)
Chapter Four: Notations (98 K)
Chapter Five: Semantics (97 K)
Chapter Six: Symbolic Functional Evaluation (82 K)
Chapter Seven: Architecture and Link to Automated Analysis (97 K)
Chapter Eight: Examples (206 K)
Chapter Nine: Conclusions (66 K)
Bibliography (67 K)
Appendices (102 K)
Send questions or comments to Nancy Day
< nday@cs.uwaterloo.ca
>