Verifikation von hybriden Systemen

Many embedded systems operate within or even comprise coupled networks of both discrete and continuous components. The behavior of such hybrid discrete-continuous systems cannot be fully understood without explicitly modeling the interaction of discrete and continuous dynamics. Tools for building such models and for simulating their dynamics are commercially available. Simulation is, however, inherently incomplete and has to be complemented by verification, which amounts to showing that the coupled dynamics of the embedded system and its environment is well-behaved, e.g. that it may never reach an undesirable state or that it will converge to a desirable state, regardless of the actual disturbance. Unfortunately, theories and tool support for verifying hybrid systems are not yet mature. Recent industrial trials, e.g. performed by Ford in the context of the Mobies initiative, indicate that current verification tools fall short with respect to both the dimensionality of the continuous state spaces and the size of the discrete state spaces they can handle. Breakthrough in both directions, thereby reconciling the seemingly contradictory demands placed by these dimensions with respect to fully symbolic representations facilitating symbolic model checking, is thus needed.