Correct Model Transformations III (CorMorant III)
Final Report Abstract
Embedded systems are ubiquitous today. Thanks to ever-increasing computing power and networking of such systems, they are capable of performing increasingly complex tasks. This complexity must be mastered through software design, which requires the use of standardized, proven software engineering methods. These include model-driven development (MDE), which guides developers from the design of abstract use cases to concrete, executable code. Since the models used here can also be very complex, support is needed to ensure that model transformations (e.g., refactoring, model synchronization, refinement, abstraction) preserve equivalent behavior and thus ensure that the abstract original models are semantically equivalent to the concrete resulting models (in terms of properties captured in both models). In particularly safety-critical areas, special quality requirements apply to trustworthiness, which necessitate formal verification of adherence to the specification and behavioral equivalences. The project aimed to develop and evaluate automated methods for the formal verification of model transformations with regard to behavioral equivalence. For the formal capture of models and model transformation programs, we considered graph transformation systems as a starting point. Within the project, we developed sophisticated correctness analysis methods for individual models, model pairs, and ultimately model transformations in several stages, based on different classes of analysis problems (result versus transformation correctness), models (varying behavior models), and model transformation specifications (operational versus relational), with a focus on behavioral equivalence and behavior refinement. Tools were developed and expanded and evaluated using case studies. As particular case study, Matlab/Simulink/Stateflow models were investigated as they play an immanent role in many safety-critical applications, e.g. in the automobile industry or in the avionics domain.
Publications
-
Toward Bridging the Gap between Formal Semantics and Implementation of Triple Graph Grammars. 2010 Workshop on Model-Driven Engineering, Verification, and Validation, 19-24. IEEE.
Giese, Holger; Hildebrandt, Stephan & Lambers, Leen
-
Toward Bridging the Gap Between Formal Semantics and Implementation of Triple Graph Grammars. Tech. rep. 37. HPI, University of Potsdam, 2010.
Holger Giese, Stephan Hildebrandt & Leen Lambers
-
Iterative Development of Consistency-Preserving Rule-Based Refactorings. Lecture Notes in Computer Science, 123-137. Springer Berlin Heidelberg.
Becker, Basil; Lambers, Leen; Dyck, Johannes; Birth, Stefanie & Giese, Holger
-
Automatic Conformance Testing of Optimized Triple Graph Grammar Implementations. Lecture Notes in Computer Science, 238-253. Springer Berlin Heidelberg.
Hildebrandt, Stephan; Lambers, Leen; Giese, Holger; Petrick, Dominic & Richter, Ingo
-
Bridging the gap between formal semantics and implementation of triple graph grammars. Software & Systems Modeling, 13(1), 273-299.
Giese, Holger; Hildebrandt, Stephan & Lambers, Leen
-
Industrial case study on the integration of SysML and AUTOSAR with triple graph grammars. Tech. rep. 57. HPI, University of Potsdam, 2012.
Holger Giese, Stephan Hildebrandt, Stefan Neumann & Sebastian Wätzoldt
-
The MDELab tool framework for the development of correct model transformations with triple graph grammars. Proceedings of the First Workshop on the Analysis of Model Transformations, 33-34. ACM.
Hildebrandt, Stephan; Lambers, Leen & Giese, Holger
-
Toward Bridging the Gap between Formal Foundations and Current Practice for Triple Graph Grammars. Lecture Notes in Computer Science, 141-155. Springer Berlin Heidelberg.
Golas, Ulrike; Lambers, Leen; Ehrig, Hartmut & Giese, Holger
-
Towards Automatic Verification of Behavior Preservation for Model Transformation via Invariant Checking. Lecture Notes in Computer Science, 249-263. Springer Berlin Heidelberg.
Giese, Holger & Lambers, Leen
-
“Attribute Handling for Bidirectional Model Transformations: The Triple Graph Grammar Case”. In: Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 49 (2012).
Leen Lambers, Stephan Hildebrandt, Holger Giese & Fernando Orejas
-
“Integration of Triple Graph Grammars and Constraints”. In: Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 54 (2012).
Stephan Hildebrandt, Leen Lambers, Basil Becker & Holger Giese
-
Complete Specification Coverage in Automatically Generated Conformance Test Cases for TGG Implementations. Lecture Notes in Computer Science, 174-188. Springer Berlin Heidelberg.
Hildebrandt, Stephan; Lambers, Leen & Giese, Holger
-
“Towards the Automatic Verification of Behavior Preservation at the Transformation Level for Operational Model Transformations”. In: Proceedings of the 4th Workshop on the Analysis of Model Transformations co-located with the 18th International Conference on Model Driven Engineering Languages and Systems (MODELS 2015), Ottawa, Canada, September 28, 2015. Ed. by Jürgen Dingel, Sahar Kokaly, Levi Lucio, Rick Salay, and Hans Vangheluwe. Vol. 1500. CEUR Workshop Proceedings. CEUR-WS.org, 2015, pp. 36–45.
Johannes Dyck, Holger Giese, Leen Lambers, Sebastian Schlesinger & Sabine Glesner
-
“Towards the verification of refactorings of hybrid simulink models”. In: Proceedings of the Third International Workshop on Verification and Program Transformation (VPT). Ed. by Andrei Nemytyk Alexei Lisitsa and Alberto Pettorossi. volume 199 of EPTCS, 2015.
Sebastian Schlesinger, Paula Herber, Thomas Göthel & Sabine Glesner
-
“Proving transformation correctness of refactorings for discrete and continuous simulink models”. In: ICONS 2016, The Eleventh International Conference on Systems, EMBEDDED 2016, International Symposium on Advances in Embedded Systems and Applications. 2016.
Sebastian Schlesinger, Paula Herber, Thomas Göthel & Sabine Glesner
-
Automatic Verification of Behavior Preservation at the Transformation Level for Relational Model Transformation. Tech. rep. 112. HPI, University of Potsdam, 2017.
Johannes Dyck, Holger Giese & Leen Lambers
-
Proving Correctness of Refactorings for Hybrid Simulink Models with Control Flow. Lecture Notes in Computer Science, 71-86. Springer International Publishing.
Schlesinger, Sebastian; Herber, Paula; Göthel, Thomas & Glesner, Sabine
-
Automatic verification of behavior preservation at the transformation level for relational model transformation. Software & Systems Modeling, 18(5), 2937-2972.
Dyck, Johannes; Giese, Holger & Lambers, Leen
-
Equivalence Checking for Hybrid Control Systems Modelled in Simulink. 2018 IEEE International Conference on Software Quality, Reliability and Security Companion (QRS-C), 572-579. IEEE.
Schlesinger, Sebastian; Herber, Paula; Gothel, Thomas & Glesner, Sabine
-
Equivalence checking of Petri net models of programs using static and dynamic cut-points. Acta Informatica, 56(4), 321-383.
Bandyopadhyay, Soumyadip; Sarkar, Dipankar & Mandal, Chittaranjan
-
“Formal verification of model refactorings for hybrid control systems”. PhD thesis. Technical University of Berlin, Germany, 2018.
Sebastian Schlesinger
-
“Verified model refactorings for hybrid control systems”. In: PhD Forum Design Automation and Test in Europe (DATE) 2018. 2018.
Sebastian Schlesinger, Paula Herber, Thomas Göthel & Sabine Glesner
-
Formal Verification of Invariants for Attributed Graph Transformation Systems Based on Nested Attributed Graph Conditions. Lecture Notes in Computer Science, 257-275. Springer International Publishing.
Schneider, Sven; Dyck, Johannes & Giese, Holger
-
“Verification of graph transformation systems with k-inductive invariants”. PhD thesis. University of Potsdam, Germany, 2020.
Johannes Dyck
-
Translation validation of coloured Petri net models of programs on integers. Acta Informatica, 59(6), 725-759.
Bandyopadhyay, Soumyadip; Sarkar, Dipankar; Mandal, Chittaranjan & Giese, Holger
