Methodologies for Application of Industrial Strength Formal Method
Dept. of Computer and
Many practitioners are interested
in new solutions. They are prepared
to listen to you and to try. However,
the key to their problems delivered
by researchers usually does not
fit, and when the practitioner comes back
complaining, he is told that it
is not the key which is wrong,
but the lock,... and the door,
and the wall...
Gerald Holzmann (ATT research)
Our contribution to the Cohsy project during 94-96 led to
an understanding of the nature of problems in the area of multi-disciplinary
development of advanced aerospace applications. Certain obstacles for integrating
formal methods in the development process were identified. These ranged
over incompatibilities between software tools, lack of adequate training
in the use of formal design and verification tools, lack of suitable tools
for designing subsystems in different engineering domains while maintaining
the ability to test the integrated product for safety-critical aspects,
and so on.
Case study based research was adopted to aid a deeper
understanding and a pedagogical dissemination of results. Certain research
level modelling and formal verification techniques were applied to
models from the JAS Gripen landing gear and hydraulics subsystems.
The current phase
In the second phase of the project (98-99) we have continued
this work with a special focus on the use of industrial strength
and verification tools. However, the case study driven research has been
performed on a fictitious example devised at Saab which apparently illustrates
certain problems appearing in real subsystems. This case study consists
of a climatic chamber in which the temperature and flow of air are subject
to regulation and monitoring in various discrete modes.
Our work in the final two years is based on
The obtained results can be summarised as follows. We propose
a methodology whereby properties of the closed loop system are proved:
using translators for transforming controller design
models directly into the format accepted by a formal verification tool;
the tool used for verification being the NPTools theorem prover for propositional
logic with integer arithmetic.
design languages in both styles of specification:
the Statechart language as a representative of the state-based
formalisms (with associated tool Statemate), and
the Lustre language as a representative of the data-flow
formalisms (with the associated tool Scade (Earlier versions: SAGA, SAO+)
modelling of the physical system using continuous modelling
environment of System-Build (MatrixX).
The latter approach builds on the knowledge of the longest
possible sampling interval as derived by the simulation models of the physical
environment. In the case of the climatic chamber, assuming a piece-wise
constant control signal which changes at equidistance points of time,
we have tranformed the non-linear environment model to a Lustre program
in a number of steps. First, assuming certain inputs to be constant or
piece-wise constant with finite range, the model of the environment was
obtained as a mode-automaton. This is an automaton where a Lustre program
is associated with each state. Next the mode-automaton is transformed to
a flat Lustre program using the traslation scheme from mode-automata to
Lustre. Thus, with a simple composition of Lustre equations for both the
controller and the physical environment a closed loop model is obtained.
This model is automatically traslated to NPTools using the tool Lucifer
in which inductive proofs for bounded response properties are easier to
To prove a safety property R (for example
that temperature will never exceed a hazardous level) we define sufficient
conditions R1, ..., Rn such that R1
& ... & Rn implies
subproperty Ri is proved either in the controller
model (using NPTools), or in the physical environment model (usig
System-Build simulations), or further decomposed into new subproperties
(see Nadjm-Tehrani 99).
To prove a timeliness property (for example that the
system will be in work mode within T seconds) we capitalize on the
synchronous model of computation for the controller.
Both the controller and its environment (as difference equations) are thus
given in the same formalism (e.g. Lustre), and subjected to bounded response
proofs using the tool Lucifer and utilising induction in NPTools.
 S. Nadjm-Tehrani. Integration of Analog and Discrete
Synchronous Design. In Hybrid Systems: Computation and Control, Proceedings
of the second international workshop, 1999, LNCS 1569, Springer Verlag,
March 99, pages 193-208.