Nicolas Rivière, Hamid Demmou, Robert Valette, Malika
Medjoudj :
LAAS-CNRS,
F-31077 Toulouse Cedex 4, France
Presented at:
16th IFAC World Congress, Prague, Czech Republic, July 3-8
2005
The purpose of the paper is to illustrate a method, based on theorem
proving, allowing the determination of a set of constraints
such that some property of an hybrid system is verified.
The approach is based on the generation of scenarios by
proving some linear logic sequents and on the analysis
of symbolic temporal constraints in a Simple Temporal Network.
In the presented example, the property is the reachability of a
given state within some temporal constraint.
Copyright: 2005 IFAC
Hybrid system, Verification, Constraint Satisfaction Problems, Petri nets
The objective of this paper is to illustrate, on a non trivial example, an approach for proving some properties of hybrid systems. The originality resides in the following points. The technique belongs to theorem proving and not to property verification. It is based on an exploration of the trajectory space (scenarios leading to some specified states) and not on state space exploration. Finally, in place of verifying a property, the approach provides a set of constraints on some parameters allowing the proof of the property. The property, considered in this paper, is that the lapse of time to reach a given state belongs to a specified domain. Only the principles of the method are given, all the technical details can be found in Nicolas Rivière's thesis. This paper focuses on the presentation of the example.