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:
Identifying and formalising the properties to prove.
Modelling the physical environment.
Applying abstraction techniques to obtain ``expressive enough''
mathematical models.
Composing the controller and environment models to obtain the
model of the closed loop system.
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:
Applying step 4 first, we get a hybrid model of the composed system.
Then we are faced with two options. Either we proceed with
verification of systems which may possibly have non-linear
developments in continuous phases,
or we abstract the model to a form for which algorithmic methods
exist.
In the latter case, we derive time-linear models of
the continuous change (in so called linear hybrid automata - LHA).
Since the problem of verifying LHA is undecidable, we
have incorporated abstraction techniques in symbolic
computations of reachable states of LHA - leading to decidable
verfication by algorithmic methods.
Since the LHA models are too coarse to accomodate
a large class of applications, work on general
models for hybrid systems for deductive reasoning
is further pursued. To this end, we propose a restriction
of hybrid transition systems which
suffice for modelling synchronous programs, their timing constraints,
and a wide range of physical systems. We discuss semantics, composition,
and progress properties for
time-deterministic hybrid transition systems
and prove certain compositionality properties.
An air control case study was provided by one of the industrial
partners in the project (SAAB aircraft AB) in the form of a textual
document and an implemented controller in an automaton based
design tool (ASA). We describe how far we have reached
in application of the above framework to this case study.
Publications:
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
S. Nadjm-Tehrani
The Air Control Case Study
Internal report. Annex A.7.1a
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