SPHINX
A Co-Evolution Framework for Model Refactoring and Proof Adaptation in Cyber-Physical Systems
| Coordinatore | UNIVERSITAT LINZ
Organization address
address: ALTENBERGERSTRASSE 69 contact info |
| Nazionalità Coordinatore | Austria [AT] |
| Totale costo | 182˙917 € |
| EC contributo | 182˙917 € |
| Programma | FP7-PEOPLE
Specific programme "People" implementing the Seventh Framework Programme of the European Community for research, technological development and demonstration activities (2007 to 2013) |
| Code Call | FP7-PEOPLE-2012-IOF |
| Funding Scheme | MC-IOF |
| Anno di inizio | 2014 |
| Periodo (anno-mese-giorno) | 2014-02-01 - 2016-04-29 |
Partecipanti
| # | ||||
|---|---|---|---|---|
| 1 |
UNIVERSITAT LINZ
Organization address
address: ALTENBERGERSTRASSE 69 contact info |
AT (LINZ) | coordinator | 182˙917.50 |
Mappa
Word cloud
Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.
Obiettivo del progetto (Objective)
'Computers that control physical processes, thus forming so-called cyber-physical systems (CPS), are today pervasively embedded into our lives. Advances in CPSs are the basis for creating environments of smart mobility, smart energy grids, telemedicine, and intelligent manufacturing. These efforts have been identified as important themes on the research agenda of the 7th Framework Programme for Research and Technological Development of the EU. 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. This overall challenge is even more aggravated by the fact that evolution is inherent to engineering CPSs due to incremental development. For example, common practice is to start with a simple CPS model, prove its correctness in a typically laborious process, and incrementally extend the model to better reflect the real-world CPS (i.e., refactor the model while ensuring preservation of safety constraints).
In order to address this challenge, especially promising techniques seem to be model-driven engineering to incrementally develop CPSs and formal verification to prove their correctness, together forming the vision of verification-driven engineering. An especially urging research question in verification-driven engineering is how to keep proofs up-to-date when models evolve.
The vision of the Sphinx project is to address this question by providing a framework supporting model refactoring and proof adaptation for CPSs, dealing in particular with three research objectives: First, support modeling and refactoring of CPSs, especially w.r.t. an extensible library of semi-automated model refactoring operations. Second, identify an initial set of refactorings and proof adaptations by incrementally building models and proofs of real-world CPSs. Third, provide an extensible library of proof adaptations, including proof recommendation techniques.'