ProofAwarE CPS - Proof-Aware Engineering of Cyber-Physical Systems

Partners: -

Funding: FWF Stand-alone Project

Employed Technologies: KeYmaera, Java, Differential Dynamic Logic

Web: http://www.cs.cmu.edu/~smitsch/index.html

Team: DI Dr. Andreas Müller, DI (FH) Dr. Stefan Mitsch, Assoc. Prof. Mag. Dr. Wieland Schwinger M.Sc., a.Univ.-Prof. Mag. Dr. Werner Retschitzegger

Motivation

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.

Problem

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.

Research Challenges

To work towards achieving this vision, we will base on our prior experience with CPS to make the concepts, methods, techniques, and tools for incremental engineering of CPS proof-aware.

• Proof-aware Refinement: Develop provably correct refinement that change the structure models (, share duplicated control decision) the behavior models (, introduce sensor uncertainty) and automatically derive proof to retain correctness.
• Proof-aware Composition: Develop provably correct composition to connect verified CPS components (, asynchronously communicate), automatically derive proof to establish system correctness and adapt components to their new environment.
• Proof-aware Implementation: Develop provably correct transformation (, non-deterministic sensor input into sensor access through a driver) that turn a CPS model into code automatically.

Evaluation

The expected benefits of the proposed research include reduced effort w.r.t. modeling, verification, and implementation of CPS, as well as increased implementation correctness. We will demonstrate the feasibility of the proposed approach with case studies in the area of road traffic and robotics, based on a proof-of-concept prototype.

Publications: