SYRF Project

Task 7: "Integration of Analog and Discrete Synchronous Design "
(Hybrid Systems)


Abstract of deliverable 7.1

Back to the SYRF Home Page



Approach:

Synchronous programs are frequently used for controlling physical devices in process control applications. To analyse such embedded systems we are often faced with properties expressed in terms of state variables in a model of the physical world These properties which are not easily verifyable using models from computer science alone, are nevertheless critical to the intended functioning of the system. The aim of the work in case studies is to increase our understanding of how to combine proof tools from the different disciplines (computer science and control engineering) in appropriate contexts.
The following 5 step plan roughly characterizes the verification process with hybrid models. Given a controller as a synchronous program, the following further activities are essential to verification of the embedded system:

  1. Identifying and formalising the properties to prove.
  2. Modelling the physical environment.
  3. Applying abstraction techniques to obtain ``expressive enough'' mathematical models.
  4. Composing the controller and environment models to obtain the model of the closed loop system.
  5. Applying algorithmic or deductive methods for verifying the properties specified under 1.
Once a mathematical model of the physical environment is available, two different strategies can be adopted based on applying steps 3 and 4 in different orders. In the project we are exploring methods in both directions. Applying step 3 first, from a DAE model we derive an abstract model of the physical system as an I/O automaton, the states of which represent flow regions in the state space of the physical system, and the input of which are control actions issued by the synchronous program. Extending the results to obtain non-deterministic I/O automata (due to effects of disturbances) is a longer term research along this track.

Achieved Results: Publications:
  1. N. Halbwachs, Y.E. Proy and P. Roumanoff
    Verification of real-time systems using linear relation analysis
    Formal Methods in System Design, vol. 11, nr. 2, pages 157-185. August 1997. Annex A.3.3.1a
  2. S. Nadjm-Tehrani The Air Control Case Study
    Internal report. Annex A.7.1a
  3. S. Nadjm-Tehrani
    Time-deterministic Hybrid Transition Systems
    In proceedings of the fifth international workshop on Hybrid Systems (HSV), September 1997. Annex A.7.1b