×

Computational techniques for the verification and control of hybrid systems. (English) Zbl 1074.93014

Capasso, Vincenzo (ed.) et al., Multidisciplinary methods for analysis optimization and control of complex systems. Lectures of the summer school Jacques Louis Lions, Montecatini, Italy, March 17–22, 2003. Berlin: Springer (ISBN 3-540-22310-X/hbk). Mathematics in Industry 7. The European Consortium for Mathematics in Industry, 151-175 (2004).
The purpose of this paper is to deal with some verification techniques for hybrid systems, a software toolkit for efficient application of these techniques, and the use of these tools in the analysis and control of large scale systems. Starting with a summary of the available methods (a detailed set of references is also given), it is observed that all rely on the ability to compute reachable sets of hybrid systems and they differ mainly in the assumptions made about the representation of sets, and evolution of the continuous state dynamics. The proposed algorithm uses an implicit surface function representation of the reachable set, and a differential game theoretic method for its evolution. Then it is illustrated how this reachable set computation may be embedded as the key component in safety verification of hybrid systems. The algorithm represents a set implicitly as the zero sublevel set of a given function, and computes its evolution through the hybrid dynamics using a combination of constrained level set methods and discrete mappings through transition functions. The algorithm is currently constrained by computational complexity, but an improved variant is taken into consideration. Two examples in the verification of protocols for aircraft collision avoidance, and of mode switching logic in autopilots finally illustrate the obtained results.
For the entire collection see [Zbl 1056.00010].

MSC:

93B40 Computational methods in systems theory (MSC2010)
93B03 Attainable sets, reachability
90B25 Reliability, availability, maintenance, inspection in operations research
93B12 Variable structure systems
93A15 Large-scale systems
93C65 Discrete event control/observation systems
93-04 Software, source code, etc. for problems pertaining to systems and control theory

Software:

SPIN; Kronos; PVS; Uppaal; HyTech
PDFBibTeX XMLCite