Anzeige
Erschienen in:
2015 | OriginalPaper | Buchkapitel
Verified Reachability Analysis of Continuous Systems
verfasst von : Fabian Immler
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Ordinary differential equations (ODEs) are often used to model the dynamics of (often safety-critical) continuous systems.
This work presents the formal verification of an algorithm for reachability analysis in continuous systems. The algorithm features adaptive Runge-Kutta methods and rigorous numerics based on affine arithmetic. It is proved to be sound with respect to the existing formalization of ODEs in Isabelle/HOL. Optimizations like splitting, intersecting and collecting reachable sets are necessary to analyze chaotic systems. Experiments demonstrate the practical usability of our developments.