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

Download


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:

    2017

  1. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer. A Benchmark for Component-based Hybrid Systems Safety Verification. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems. Goran Frehse and Matthias Althoff, editors, 48 of EPiC Series in Computing, pages: 65-74. EasyChair, April, 2017. BibTeX
    @inproceedings{ARCH17:Benchmark_for_Component_based_Hybrid,
       title = {A Benchmark for Component-based Hybrid Systems Safety Verification},
       author = {Andreas M{\"u}ller and Stefan Mitsch and Werner Retschitzegger and Wieland Schwinger and Andr{\'e} Platzer},
       year = {2017},
       publisher = {EasyChair},
       booktitle = {4th International Workshop on Applied Verification of Continuous and Hybrid Systems},
       pages = {65-74},
       volume = {48 },
       month = {04},
       series = {EPiC Series in Computing}
    }
  2. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer. Change and Delay Contracts for Hybrid System Component Verification. Fundamental Approaches to Software Engineering - 20th International Conference, FASE 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings. Marieke Huisman and Julia Rubin, editors, Uppsala, Sweden,10202 of Lecture Notes in Computer Science, pages: 134--151. April, 2017. BibTeX
    @inproceedings{DBLP:conf/fase/0002MRSP17,
       title = {Change and Delay Contracts for Hybrid System Component Verification},
       author = {Andreas M{\"{u}}ller and Stefan Mitsch and Werner Retschitzegger and Wieland Schwinger and Andr{\'{e}} Platzer},
       year = {2017},
       booktitle = {Fundamental Approaches to Software Engineering - 20th International Conference, {FASE} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Proceedings},
       pages = {134--151},
       volume = {10202 },
       month = {04},
       series = {Lecture Notes in Computer Science},
       address = {Uppsala, Sweden}
    }
  3. 2016

  4. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, André Platzer. A Component-Based Approach to Hybrid Systems Safety Verification. Integrated Formal Methods - 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings. Erika {\'{A}}brah{\'{a}}m and Marieke Huisman, editors, Reykjavik, Iceland,9681 of Lecture Notes in Computer Science, pages: 441--456. Springer, June, 2016. PDF BibTeX
    @inproceedings{DBLP:conf/ifm/MullerMRSP16,
       title = {A Component-Based Approach to Hybrid Systems Safety Verification},
       author = {Andreas M{\"{u}}ller and Stefan Mitsch and Werner Retschitzegger and Wieland Schwinger and Andr{\'{e}} Platzer},
       year = {2016},
       publisher = {Springer},
       booktitle = {Integrated Formal Methods - 12th International Conference, {IFM} 2016, Reykjavik, Iceland, June 1-5, 2016, Proceedings},
       pages = {441--456},
       volume = {9681 },
       month = {06},
       series = {Lecture Notes in Computer Science},
       address = {Reykjavik, Iceland}
    }
  5. 2015

  6. Andreas Müller, Stefan Mitsch, André Platzer. Verified Traffic Networks: Component-Based Verification of Cyber-Physical Flow Systems. IEEE 18th International Conference on Intelligent Transportation Systems, ITSC 2015, Gran Canaria, Spain, September 15-18, 2015. Gran Canaria, Spain,pages: 757--764. IEEE, September, 2015. PDF BibTeX
    @inproceedings{DBLP:conf/itsc/0002MP15,
       title = {Verified Traffic Networks: Component-Based Verification of Cyber-Physical Flow Systems},
       author = {Andreas M{\"{u}}ller and Stefan Mitsch and Andr{\'{e}} Platzer},
       year = {2015},
       publisher = {IEEE},
       booktitle = {{IEEE} 18th International Conference on Intelligent Transportation Systems, {ITSC} 2015, Gran Canaria, Spain, September 15-18, 2015},
       pages = {757--764},
       month = {09},
       address = {Gran Canaria, Spain}
    }
  7. Andreas Müller. Component-based CPS Verification: A Recipe for Reusability. Doctoral Symposium of Formal Methods, co-located with the 20th International Symposium on Formal Methods (FM 2015). Oslo, Norway,pages: 33-37. June, 2015. PDF BibTeX
    @inproceedings{Mueller2015,
       title = {{Component-based CPS Verification: A Recipe for Reusability}},
       author = {Andreas M{\"{u}}ller},
       year = {2015},
       booktitle = {Doctoral Symposium of Formal Methods, co-located with the 20th International Symposium on Formal Methods (FM 2015)},
       pages = {33-37},
       month = {06},
       address = {Oslo, Norway}
    }