Methodologies for Application of Industrial Strength Formal Method

Simin Nadjm-Tehrani
Real-time 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 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 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 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 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₁, ..., R_nsuch that R₁ & ... & R_nimplies R. Each subproperty R_i 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 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 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 perform.

References:

[1] 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.