by Holger Giese, Leen Lambers
Abstract:
Graph transformation can be used as a formal foundation for modeling different kinds of evolving graph structures. In particular, we present two application domains, cyber-physical systems (CPS) and model-driven engineering (MDE), where graph transformation has been used successfully to formally model different scenarios. Furthermore, we employ inductive invariant checking for graph transformation as a verification technique for the different scenarios of the two domains. In the CPS domain the invariance of important safety properties can be shown. In the MDE domain, behavior preservation of model transformations can be reduced to invariant checking. We give an overview of how invariant checking has been applied in these two domains on different scenarios. We present the strengths and weaknesses of this verification technique and conclude with some open challenges.
Reference:
Invariant Checking for Graph Transformation: Applications & Open Challenges (Abstract) (Holger Giese, Leen Lambers), In Verification of Evolving Graph Structures, Dagstuhl, Germany (Parosh Aziz Abdulla, Fabio Gadducci, Barbara König, Viktor Vafeiadis, eds.), Dagstuhl Publishing, volume 5, 2016.
Bibtex Entry:
@InProceedings{GL16,
AUTHOR = {Giese, Holger and Lambers, Leen},
TITLE = {{Invariant Checking for Graph Transformation: Applications & Open Challenges (Abstract)}},
YEAR = {2016},
MONTH = {March},
BOOKTITLE = {Verification of Evolving Graph Structures, Dagstuhl, Germany},
VOLUME = {5},
NUMBER = {11},
PAGES = {11-11},
EDITOR = {Abdulla, Parosh Aziz and Gadducci, Fabio and König, Barbara and Vafeiadis, Viktor},
SERIES = {Dagstuhl Reports},
ADDRESS = {Dagstuhl, Germany},
PUBLISHER = {Dagstuhl Publishing},
URL = {http://dx.doi.org/10.4230/DagRep.5.11.1},
ABSTRACT = {Graph transformation can be used as a formal foundation for modeling different kinds of evolving graph structures. In particular, we present two application domains, cyber-physical systems (CPS) and model-driven engineering (MDE), where graph transformation has been used successfully to formally model different scenarios. Furthermore, we employ inductive invariant checking for graph transformation as a verification technique for the different scenarios of the two domains. In the CPS domain the invariance of important safety properties can be shown. In the MDE domain, behavior preservation of model transformations can be reduced to invariant checking. We give an overview of how invariant checking has been applied in these two domains on different scenarios. We present the strengths and weaknesses of this verification technique and conclude with some open challenges.}
}