2009 | OriginalPaper | Buchkapitel
HybridFluctuat: A Static Analyzer of Numerical Programs within a Continuous Environment
verfasst von : Olivier Bouissou, Eric Goubault, Sylvie Putot, Karim Tekkal, Franck Vedrine
Erschienen in: Computer Aided Verification
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
A new static analyzer is described, based on the analyzer Fluctuat. Its goal is to synthetize invariants for hybrid systems, encompassing a continuous environment described by a system of possibly switched ODEs, and an ANSI C program, in interaction with it. The evolution of the continuous environment is over-approximated using a guaranteed integrator that we developped, and special assertions are added to the program that simulate the action of sensors and actuators, making the continuous environment and the program communicate. We demonstrate our approach on an industrial case study, a part of the flight control software of ASTRIUM’s Automated Transfer Vehicle (ATV).