Methodologies for Application of Industrial Strength Formal Method
Simin NadjmTehrani
Realtime Systems
Laboratory (RTSLAB)
Dept. of Computer and
Information Science
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)
Background
Our contribution to the Cohsy project during 9496 led to
an understanding of the nature of problems in the area of multidisciplinary
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 safetycritical 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 (9899) we have continued
this work with a special focus on the use of industrial strength
specification
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

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 statebased
formalisms (with associated tool Statemate), and

the Lustre language as a representative of the dataflow
formalisms (with the associated tool Scade (Earlier versions: SAGA, SAO+)

modelling of the physical system using continuous modelling
environment of SystemBuild (MatrixX).
The obtained results can be summarised as follows. We propose
a methodology whereby properties of the closed loop system are proved:

To prove a safety property R (for example
that temperature will never exceed a hazardous level) we define sufficient
conditions R_{1}, ..., R_{n }such that R_{1}
& ... & R_{n }implies
R. Each
subproperty R_{i } is proved either in the controller
model (using NPTools), or in the physical environment model (usig
SystemBuild simulations), or further decomposed into new subproperties
(see NadjmTehrani 99).

To prove a timeliness property (for example that the
system will be in work mode within T seconds) we capitalize on the
underlying
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.
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 piecewise
constant control signal which changes at equidistance points of time,
we have tranformed the nonlinear environment model to a Lustre program
in a number of steps. First, assuming certain inputs to be constant or
piecewise constant with finite range, the model of the environment was
obtained as a modeautomaton. This is an automaton where a Lustre program
is associated with each state. Next the modeautomaton is transformed to
a flat Lustre program using the traslation scheme from modeautomata 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
perform.
References:
[1] S. NadjmTehrani. 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 193208.