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

Partners: -

Funding: Marie Curie IOF

Employed 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: