Abstract interpretation of the physical inputs of embedded programs

Abstract

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. © 2008 Springer-Verlag Berlin Heidelberg.