Abstract
We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. With this compositional approach we exploit locality in system designs. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control and car control.
Document type: Part of book or chapter of book
Full document
Original document
The different versions of the original document can be found in:
DOIS: 10.1184/r1/6604349.v1 10.1007/s10703-009-0079-8 10.1007/978-3-540-70545-1_17 10.1184/r1/6604346.v1 10.1184/r1/6604346 10.1184/r1/6604349 10.21236/ada476791
Document information
Published on 01/01/2009
Volume 2018, 2009
DOI: 10.1184/r1/6604349.v1
Licence: CC BY-NC-SA license
Share this document
Keywords
claim authorship
Are you one of the authors of this document?