Interval Analysis Applied to Model-Checking of Embedded Control Systems

Model-checking is a search technique that explores the state space of a modeled system looking for states that match specific criteria. The criteria can be anything from simple assertions to complex sequences of states or events. In effect, the model-checker allows the user to exhaustively debug a model by examining it for scenarios that cause particular undesirable behaviors. Model-checkers generally rely on Boolean values, enumerations and small integer ranges to make the state space search tractable. Where possible, abstraction techniques are used in the process of building the model to further reduce the state space. For example, a property of an open-loop controller may depend on the relationship between the continuously-varying input and a static threshold.