Proof-Aware Engineering of Cyber-Physical Systems

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 operations that change the structure of models (e.g., share duplicated control decision) or the behavior of models (e.g., introduce sensor uncertainty) and automatically derive proof obligations to retain correctness. Proof-aware Composition: Develop provably correct composition operators to connect verified CPS components (e.g., asynchronously communicate), automatically derive proof obligations to establish overall system correctness and adapt components to their new environment. Proof-aware Implementation: Develop provably correct transformation operators (e.g., 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.

Cyber-physical systems in road traffic, aircraft, robotics, medical devices, and many other safety-critical areas ask for highest safety standards. The project ProofAwareCPS developed modeling and theorem proving techniques to assemble cyber-physical systems from components with mathematical proof in a way that lifts proofs about components to full system-level proofs about the emerging behavior of the interacting components in a cyber-physical system. A unique characteristic of cyber-physical systems is their combined computer-based control decisions (e.g., how to control the brakes, throttle, and steering in a self-driving car) and the entailed physical motion (e.g., how the car itself moves in reaction to those decisions) in relation to other agents in the system's environment (e.g., pedestrians crossing streets). ProofAwareCPS targeted a comprehensive approach for such hybrid software-controlled physical behavior and the project results apply specifically not only to the control software, but also to the physical behavior. As fundamental pillars of the approach, ProofAwareCPS studied three topics: proof-aware composition, proof-aware refinement, and proof-aware implementation. Proof-aware composition exploits the structure of templates for describing components and their interaction to provide a proof technique to lift component proofs to system proofs; the proof technique can be (and is) implemented as a proof tactic in theorem provers for cyber-physical systems to automate compositional verification. Proof-aware refinement describes techniques to develop and adapt systems and proofs incrementally, which is not only useful for model and proof maintenance, but also at the heart of the generic composition proof developed in the project. Proof-aware implementation tackles translation from component models into executable control and monitoring software in a popular programming language for immediate practical applicability of verified models of cyber-physical systems. The project results facilitate distributed, model-based development of cyber-physical systems with safety guarantees. The developed modeling and proof techniques were demonstrated with modeling and verification case studies in the area of road traffic control and collision avoidance in robotics.