Approach:

This report deals with analysis methods for hybrid systems.  We treat two techniques for analysing  safety and timeliness:

• Formal verification methods based on a combination of theorem proving and simulation. We continue the approach in deliverable 7.2  whereby transformations on the non-linear plant equation are used to arrive at models which are input to a theorem prover - in this case the first order theorem prover NP-Tools. This approach is concretely based on the language of Lustre and related tools and concepts, but conceptually it should be equally applicable to the language of Signal.

• Co-simulation of the plant and the controller making up the hybrid system. Here we analyse the hybrid model where the plant is modelled in a continuous environment (specifically Matlab-Simulink) and the discrete controller in a synchronous language (specifically Signal). The approach builds on automatic generation of C-code in order to run in a pseudo parallel manner.

Acheived Results:

The above techniques were applied and illustrated on two case studies, including the climatic chamber case we physically modelled in deliverable 7.1.

• For proofs of safety properties we propose the use of compositional reasoning, A property is decomposed in subproperties whereby each subproperty is formally proved in the controller (by theorem proving), in the plant (by continuous analysis and simulation), or further decomposed. We have experimented with translators from Lustre and Statemate to theorem prover models in NP-Tools.
• For formal proofs of timeliness properties we further need to represent the model of the plant in a format acceptable to verification tools. The climatic chamber case study is used to show how restrictions on some inputs to the (non-linear) plant model can be used to derive models in NP-Tools by a number of transformations (see Annex.7.3.A). Bounded response proofs on the composed model are based on induction over automatically generated models of the system in NP-Tools, using the tool Lucifer.
• For analysis of the closed loop system using co-simulation, we have studied the modes of communication between C-processes representing  components in the plant and the  controller. A co-simulation environment  has been built, based on the code generation capabilities of  Signal and Simulink. This environment has been used to model and analyse a siphon pump machine originally proposed by the Swedish engineer Christopher Polhem.

• Nadjm-Tehrani S., Åkerlund O. (1999). Combining theorem proving and continuous models in synchronous design   In proceedings of the World Congress on Formal Methods, Tolouse, France, September 1999, Volume II, LNCS 1709, pages 1384-1399, (C) Springer Verlag.
• Nadjm-Tehrani S. (1999). Integration of Analog and Discrete Synchronous Design  In proceedings of the second international workshop on Hybrid Systems: Computation and Control, Nijmegen, Netherlands, March 1999, LNCS 1569, (C) Springer Verlag , pages 193-208.
• Turodet S., Nadjm-Tehrani S., Benveniste A., Strömberg J-E. (1999). Co-simulation of Signal-Simulink, Submitted for publication. Annex.7.3.B
• Nadjm-Tehrani S. Transformations with "The big L approach", Internal report , Annex.7.3.A