Automated Formal Verification of Model Transformations

TitleAutomated Formal Verification of Model Transformations
Publication TypeConference Paper
Year of Publication2003
AuthorsVarró, D., and Pataricza, A.
EditorJürjens, J., Rumpe, B., France, R., and Fernandez, E. B.
Conference NameCSDUML 2003: Critical Systems Development in UML; Proceedings of the UML'03 Workshop
Date PublishedSeptember
PublisherTechnische Universität München
AbstractWhen designing safety critical applications in UML, the system models are frequently projected into various mathematical domains (such as Petri nets, transition systems, process algebras, etc.) to carry out a formal analysis of the system under design by \emph{automatic model transformations}. Automation surely increases the quality of such transformations as errors manually implanted into transformation programs during implementation are eliminated; however, conceptual flaws in transformation design still remain undetected. In this paper, we present a model-level, modeling language independent and highly automated technique to formally verify by model checking that a model transformation from an arbitrary well-formed model instance of the source modeling language into its target equivalent preserves (language specific) dynamic consistency properties. We demonstrate the feasibility of our approach on a complex mathematical model transformation from UML statecharts to Petri nets.