Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Abstract Interpretation of the Physical Inputs of Embedded Programs
verfasst von : Olivier Bouissou, Matthieu Martel
Erschienen in: Verification, Model Checking, and Abstract Interpretation
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
We define an abstraction of the continuous variables that serve as inputs to embedded software. In existing static analyzers, these variables are most often abstracted by a constant interval, and this approach has shown its limits. We propose a different method that analyzes in a more precise way the continuous environment. This environment is first expressed as the semantics of a special continuous program, and we define a safe abstract semantics. We introduce the abstract domain of interval valued step functions and show that it safely over-approximates the set of continuous functions. The theory of guaranteed integration is then used to effectively compute an abstract semantics and we prove that this abstract semantics is safe.