A Co-Evolution Framework for Model Refactoring and Proof Adaptation in Cyber-Physical Systems

Download


Partners: -

Funding: Marie Curie IOF

Eymployed Technologies: -

Web:

Team: DI (FH) Dr. Stefan Mitsch


Overview

Motivation

Computers that control physical processes, thus forming so-called cyber-physical systems (CPS), are today pervasively embedded into our lives. For example, cars equipped with adaptive cruise control form a typical CPS, responsible for controlling acceleration on the basis of distance sensors. Further prominent examples can be found in many safety-critical areas, such as in factory automation, medical equipment, automotive, aviation, and railway industries. From an engineering viewpoint, CPSs can be described in a hybrid manner in terms of discrete control decisions (the cyber-part, e.g., setting the acceleration of a car to keep safety distance) and in terms of dierential equations modeling the entailed continuous dynamics of the physical world under control (the physical part, e.g., motion).

Challenge

The key challenge in engineering CPSs is the question of how to ensure their correct functioning in order to avoid incorrect control decisions w.r.t. safety requirements (e.g., a car with adaptive cruise control will never collide with a car driving ahead). This overall challenge is even reinforced by the fact that evolution is inherent to engineering CPSs due to incremental development being frequently applied to cope with their complexity. For example, common practice is to start with a simple CPS model (e.g., apply only maximum braking power), prove its correctness in a typically laborious process, and incrementally extend the model (e. g., choose between maximum and moderate braking power) to better reflect the real-world CPS (i. e., refactor the model while ensuring preservation of safety constraints).

Vision

The vision of the Sphinx project is to address this question by providing a co-evolution framework for verication-driven engineering supporting model refactoring and corresponding proof adaptation for CPSs. In particular, we will deal with the following research objectives:

CPS modeling and refactoring

The first research question is how to support modeling of CPSs and evolution of these models with recurring refactorings in a way that is amenable to proof adaptation. Let us revisit our adaptive cruise control example, in which an initial model that applied maximum braking power only was modied to support moderate braking too. Such model evolution typically requires multiple low-level refactoring operations: in our example, we have to (i) introduce a constant for moderate braking power, (ii) split a previous deterministic control choice into two exclusive ones, and (iii) derive exclusive conditions along the moderate braking power from the condition that triggered the previous control choice. In a more generic manner, these low-level operations could be formulated to contribute to a composite operation (e.g., exclusive control decision split). Since such composite operations, in our experience, are of recurring nature, they should be assembled into a library of model refactoring operations, thereby facilitating re-use. The objective, thus, is to enable CPS modelers to define and manage their own refactoring operations, and let them semi-automatically evolve CPS models by executing these refactoring operations.

Operation and impact detection

The second research goal of Sphinx is to determine an initial catalog of dierent kinds of refactoring operations that may occur in models of CPSs, and their impact on verication. For example, refactoring of control decisions or safety constraints may lead to additional/unnecessary proof branches, or refactoring of dynamics and extension of the system may require additional proofs basing on previous ones as lemmata. The research objective is to extend existing work on evolution in diverse research fields with model refactoring operations and their impact on verication found specically in CPS engineering. For the latter, we will model and verify CPSs that will be developed in collaboration with experts from road traffic control and robotics. From a technical viewpoint, we have semi-automatically find differences in incrementally built CPS models and proofs, and relate those differences to each other (i.e., support proof impact labeling).

Proof Adaptation

The third research question is how to properly adapt proofs according to model refactorings. The objective is to support CPS modelers in dening proof adaptation operations, selecting appropriate operations from a repository, and semi-automatically adapting existing proofs. Such proof adaptation operations are envisioned in Sphinx in dierent forms: rst, a proof skeleton of previously verified branches that re-occur in the refactored model can be built, thus sparing the eort of re-verication of exact matches. Second, previous proofs may be used as lemmata (e.g., a proof of two cars being safe may be the basis for proving safety of unbounded many cars). Finally, proof strategies and cuts that were employed to guide previous verication could be re-used in new proofs.

The Sphinx Verification-Driven Engineering Toolkit

Sphinx is an extensible verification-driven engineering toolkit based on the Eclipse platform. It provides textual and graphical modeling editors to describe the structure, the discrete dynamics, and the continuous dynamics of cyber-physical systems. Sphinx uses KeYmaera as hybrid verification tool.

 

Sphinx includes

  • Textual editor for hybrid programs and theorems in Differential Dynamic Logic, which can be verified using KeYmaera
  • Textual editor for proofs created in KeYmaera
  • UML profile that defines a graphical notation for hybrid programs and theorems
  • Model-to-text transformation, which turns UML models into theorems in Differential Dynamic Logic
  • Sourcecode version access to exchange models, theorems, and (partial) proofs, including proof comparison
  • Export of (partial) proofs
  • Export of hybrid programs and theorems in Differential Dynamic Logic to LaTeX
  • Import of Geometric Relevance Filtering results
  • Collaboration and task planning

Installation

    1. Start Eclipse Juno
    2. Click Help->Install new Software...
    3. Click Add to add the Papyrus update site
    4. Type the following into the location of the update site
http://download.eclipse.org/modeling/mdt/papyrus/updates/releases/juno
    1. Click Add to add the Sphinx update site
    2. Type the following into the location of the update site
http://www.cis.jku.at/sphinx/updates/releases
  1. Follow the screen instructions to complete the installation

User Manual

The Sphinx user manual can be downloaded here.

News

  • 04/09/2013: Sphinx is presented at HSCC
  • 04/05/2013: New publication about collaborative verification of cyber-physical systems

Publications:

    2015

  1. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, André Platzer. KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems. Automated Deduction - CADE-25 . Amy P. Felty and Aart Middeldorp, editors, 9195of Lecture Notes in Computer Science, pages: 527--538. Springer, August, 2015. BibTeX
    @inproceedings{DBLP:conf/cade/FultonMQVP15,
       title = {{KeYmaera X}: An Axiomatic Tactical Theorem Prover for Hybrid Systems},
       author = {Nathan Fulton and Stefan Mitsch and Jan{-}David Quesel and Marcus V{\"{o}}lp and Andr{\'{e}} Platzer},
       year = {2015},
       publisher = {Springer},
       booktitle = {Automated Deduction - {CADE-25} },
       pages = {527--538},
       volume = {9195},
       month = {08},
       note = {http://www.cs.cmu.edu/~smitsch/pdf/keymaerax.pdf},
       series = {Lecture Notes in Computer Science}
    }
  2. Jan-David Quesel, Stefan Mitsch, Sarah Loos, Nikos Aréchiga, André Platzer. How to Model and Prove Hybrid Systems with KeYmaera: A Tutorial on Safety. STTT. :26. 2015. BibTeX
    @article{DBLP:journals/sttt/QueselMLAP15,
       title = {How to Model and Prove Hybrid Systems with {KeYmaera}: A Tutorial on Safety},
       author = {Jan-David Quesel and Stefan Mitsch and Sarah Loos and Nikos Ar{\'e}chiga and Andr{\'e} Platzer},
       journal = {STTT},
       year = {2015},
       pages = {26},
       note = {http://www.cs.cmu.edu/~smitsch/pdf/KeYmaera-tutorial.pdf}
    }
  3. Stefan Mitsch, André Platzer, Werner Retschitzegger, Wieland Schwinger. Logic-based modeling approaches for qualitative and hybrid reasoning in dynamic spatial systems. ACM Computing Surveys. 48(1):3:1--3:40. 2015. BibTeX
    @article{DBLP:journals/csur/MitschPRS15,
       title = {Logic-based modeling approaches for qualitative and hybrid reasoning in dynamic spatial systems},
       author = {Stefan Mitsch and Andr{\'e} Platzer and Werner Retschitzegger and Wieland Schwinger},
       journal = {ACM Computing Surveys},
       year = {2015},
       pages = {3:1--3:40},
       volume = {48},
       number = {1},
       note = {http://www.cs.cmu.edu/~smitsch/pdf/surveydynamicspatial.pdf}
    }
  4. 2014

  5. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger. A Conceptual Reference Model of Modeling and Verification Concepts for Hybrid Systems. Proceedings of the 7th International Conference on Knowledge Science, Engineering and Management. Sibiu, Romania, Springer, October, 2014. PDF BibTeX
    @inproceedings{Mueller2014,
       title = {{A Conceptual Reference Model of Modeling and Verification Concepts for Hybrid Systems}},
       author = {Andreas M{\"{u}}ller and Stefan Mitsch and Werner Retschitzegger and Wieland Schwinger},
       year = {2014},
       publisher = {Springer},
       booktitle = {Proceedings of the 7th International Conference on Knowledge Science, Engineering and Management},
       month = {10},
       address = {Sibiu, Romania}
    }
  6. Stefan Mitsch, Jan-David Quesel, André Platzer. From Safety to Guilty and from Liveness to Niceness. Proceedings of the 5th Workshop on Formal Methods for Robotics and Automation. Berkeley, CA, USA, July, 2014. PDF BibTeX
    @inproceedings{Mitsch2014a,
       title = {{From Safety to Guilty and from Liveness to Niceness}},
       author = {Stefan Mitsch and Jan-David Quesel and Andr{\'e} Platzer},
       year = {2014},
       booktitle = {Proceedings of the 5th Workshop on Formal Methods for Robotics and Automation},
       month = {07},
       address = {Berkeley, CA, USA}
    }
  7. Stefan Mitsch, Jan-David Quesel, André Platzer. Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid Systems. Proceedings of the 19th International Symposium on Formal Methods (FM). Singapore, Springer, May, 2014. PDF BibTeX
    @inproceedings{Mitsch2014,
       title = {{Refactoring, Refinement, and Reasoning - A Logical Characterization for Hybrid Systems}},
       author = {Stefan Mitsch and Jan-David Quesel and Andr{\'e} Platzer},
       year = {2014},
       publisher = {Springer},
       booktitle = {Proceedings of the 19th International Symposium on Formal Methods (FM)},
       month = {05},
       address = {Singapore}
    }
  8. Stefan Mitsch, Grant Olney Passmore, André Platzer. Collaborative Verification-Driven Engineering of Hybrid Systems. Mathematics in Computer Science. 8(1):71-97. March, 2014. PDF BibTeX
    @article{Mitsch2014c,
       title = {{Collaborative Verification-Driven Engineering of Hybrid Systems}},
       author = {Stefan Mitsch and Grant Olney Passmore and Andr{\'e} Platzer},
       journal = {Mathematics in Computer Science},
       year = {2014},
       pages = {71-97},
       volume = {8},
       number = {1},
       month = {03}
    }
  9. 2013

  10. Stefan Mitsch, Khalil Ghorbal, André Platzer. On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles. Robotics: Science and Systems IX. 2013. PDF BibTeX
    @inproceedings{Mitsch2013a,
       title = {{On Provably Safe Obstacle Avoidance for Autonomous Robotic Ground Vehicles}},
       author = {Stefan Mitsch and Khalil Ghorbal and Andr{\'e} Platzer},
       year = {2013},
       booktitle = {Robotics: Science and Systems IX}
    }
  11. Stefan Mitsch, Grant Olney Passmore, André Platzer. A Vision of Collaborative Verification-Driven Engineering of Hybrid Systems. Proceedings of Enabling Domain Experts to use Formalised Reasoning - Symposium AISB, Do-Form. Manfred Kerber and Christoph Lange and Colin Rowat, editors, pages: 8-17. 2013. PDF BibTeX
    @inproceedings{Mitsch2013b,
       title = {{A Vision of Collaborative Verification-Driven Engineering of Hybrid Systems}},
       author = {Stefan Mitsch and Grant Olney Passmore and Andr{\'e} Platzer},
       year = {2013},
       booktitle = {Proceedings of Enabling Domain Experts to use Formalised Reasoning - Symposium AISB, Do-Form},
       pages = {8-17}
    }
  12. 2012

  13. Stefan Mitsch, Sarah M. Loos, André Platzer. Towards Formal Verification of Freeway Traffic Control. Proceedings of ACM/IEEE Third International Conference on Cyber-Physical Systems. Chenyang Lu, editors, pages: 171-180. IEEE, 2012. PDF BibTeX
    @inproceedings{Mitsch2012,
       title = {{Towards Formal Verification of Freeway Traffic Control}},
       author = {Stefan Mitsch and Sarah M. Loos and Andr{\'e} Platzer},
       year = {2012},
       publisher = {IEEE},
       booktitle = {Proceedings of ACM/IEEE Third International Conference on Cyber-Physical Systems},
       pages = {171-180}
    }