Partners: -
Funding: Marie Curie IOF
Employed Technologies: -
Team: DI (FH) Dr. Stefan Mitsch
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).
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).
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:
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.
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).
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.
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
http://download.eclipse.org/modeling/mdt/papyrus/updates/releases/juno
http://www.cis.jku.at/sphinx/updates/releases
The Sphinx user manual can be downloaded here.
Publications:
@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} - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
pages = {527--538},
volume = {9195},
month = {08},
note = {http://www.cs.cmu.edu/~smitsch/pdf/keymaerax.pdf},
series = {Lecture Notes in Computer Science}
}
@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},
note = {http://www.cs.cmu.edu/~smitsch/pdf/KeYmaera-tutorial.pdf}
}
@article{DBLP:journals/csur/MitschPRS15-copy,
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}
}
@inproceedings{DBLP:conf/ksem/MullerMRS14,
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 = {Knowledge Science, Engineering and Management - 7th International Conference, {KSEM} 2014, Sibiu, Romania, October 16-18, 2014. Proceedings},
pages = {368--379},
month = {10},
address = {Sibiu, Romania}
}
@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}
}
@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}
}
@article{DBLP:journals/mics/MitschPP14,
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}
}
@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}
}
@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}
}
@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}
}