Runtime Verification of Hybrid Systems with Affine Arithmetic Decision Diagrams

Inhalt:
A novel approach for runtime verification of hybrid systems is presented. The approach uses Affine Arithmetic Decision Diagrams to describe and compute the reachable state space of a model of a hybrid system, and to generate monitors. The monitors can be used during runtime to check the consistency of observed signal trajectories against the possible dynamic behavior of the model. The consistency check is formulated as a linear programming problem.