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.


Original document

The different versions of the original document can be found in:

http://dx.doi.org/10.1007/978-3-540-70545-1_17
http://link.springer.com/article/10.1007/s10703-009-0079-8/fulltext.html,
http://link.springer.com/content/pdf/10.1007/s10703-009-0079-8,
http://dx.doi.org/10.1007/s10703-009-0079-8 under the license http://www.springer.com/tdm
https://link.springer.com/article/10.1007/s10703-009-0079-8,
http://oai.dtic.mil/oai/oai?verb=getRecord&metadataPrefix=html&identifier=ADA476797,
http://repository.cmu.edu/compsci/1244,
https://users.ece.cmu.edu/~krogh/otherNSFpapers/PlC08.pdf,
https://dblp.uni-trier.de/db/journals/fmsd/fmsd35.html#PlatzerC09,
https://www.researchgate.net/profile/Andre_Platzer/publication/226247835_Computing_differential_invariants_of_hybrid_systems_as_fixedpoints/links/00463537caa7ef05ff000000.pdf,
https://www.scipedia.com/public/Platzer_Clarke_2009a,
https://apps.dtic.mil/dtic/tr/fulltext/u2/a476797.pdf,
https://dl.acm.org/citation.cfm?id=1612944,
https://apps.dtic.mil/docs/citations/ADA476797,
https://doi.org/10.1007/s10703-009-0079-8,
https://rd.springer.com/article/10.1007/s10703-009-0079-8,
https://academic.microsoft.com/#/detail/2106606898
https://dblp.uni-trier.de/db/conf/cav/cav2008.html#PlatzerC08,
http://dx.doi.org/10.1007/978-3-540-70545-1_17,
https://rd.springer.com/chapter/10.1007/978-3-540-70545-1_17,
https://dl.acm.org/citation.cfm?id=1427805,
https://doi.org/10.1007/978-3-540-70545-1_17,
https://academic.microsoft.com/#/detail/3021664313



DOIS: 10.1007/s10703-009-0079-8 10.1184/r1/6604346.v1 10.1007/978-3-540-70545-1_17 10.21236/ada476791 10.1184/r1/6604349.v1 10.1184/r1/6604346 10.1184/r1/6604349

Back to Top

Document information

Published on 01/01/2009

Volume 2018, 2009
DOI: 10.1184/r1/6604349.v1
Licence: CC BY-NC-SA license

Document Score

0

Views 0
Recommendations 0

Share this document

claim authorship

Are you one of the authors of this document?