![]() |
Formal
Validation of System Specifications
presented by
Nancy Day
|
formalWARE
project
formalWARE
formalWARE
|
Presented by Nancy Day at
formalWARE's Open House
on October 8, 1997 at Cecil
Green House, UBC.
This research focuses on techniques for systematically analyzing specifications using techniques such as simulation, prototyping, checking for completeness and consistency and model checking. Model checking allows us to query the specification to see if it has certain desired properties. To test these ideas, Day has built a framework in which different notations can be used to describe different parts of a system, but integrated to create an overall model of the system's behavior for analysis. She has found that using an explicit formal definition of the meaning of the notations makes it possible to do this integration. This formal definition can then be used to drive the analysis. This framework has been used to run completeness
and consistency checks on the
Separation Minima for the North Atlantic Region
given in a tabular specification
notation. A second example in progress is the analysis
of an aeronautical telecommunications network specified in a state
transition notation.
Presentation
Slides (HTML)
. |