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)


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

The obtained results can be summarised as follows. We propose a methodology whereby properties of the closed loop system are proved:
  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.


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