Invariant Checking for Graph Transformation: Applications & Open Challenges
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.