Cyber-physical systems (CPS) are operated in many safety-critical areas where lives are at stake, such as in road traffic and robotics. CPS are almost impossible to get right without proper analysis of their behavior, which emerges from combined discrete dynamics (the cyber part, e.g., setting the acceleration of a car) and the entailed continuous dynamics (the physical part, e.g., motion of a car). Thus, formal verification techniques to analyze CPS are of paramount importance to provide correctness guarantees for all of the infinitely many possible states of a CPS - not just for some, as in testing or simulation.
Formal verification rests on models of a CPS, which capture these infinitely many possible states. Current methods make a trade-off between full automation and modeling expressiveness: Reachability analysis methods focus on full automation and are therefore restricted to less expressive classes of CPS. Theorem proving methods, in contrast, rely on human guidance to make progress despite undecidability so that more realistic models can be verified. To make human guidance possible, however, the inherent complexities of CPS practically mandate incremental development, which requires full re-verification after every change with current theorem proving methods. At the same time, we want the correctness properties that are verified formally for a model also to hold for an actual implementation. For this, we have to resolve a gap between modeling concepts that are beneficial for verification (e.g., non-deterministic control) and those that are appropriate for implementation (e.g., deterministic control) in a way that preserves correctness.
The vision of this project is to reduce verification effort despite incremental CPS engineering, and at the same time ensure implementation correctness despite conceptual gaps to modeling.