Automated Formal Verification of Model Transformations

CímAutomated Formal Verification of Model Transformations
Közlemény típusaConference Paper
Kiadás éve2003
SzerzőkVarró, D., and Pataricza, A.
SzerkesztőJürjens, J., Rumpe, B., France, R., and Fernandez, E. B.
Konferencia neveCSDUML 2003: Critical Systems Development in UML; Proceedings of the UML'03 Workshop
Kiadás dátumaSeptember
KiadóTechnische Universität München
ÖsszefoglalásWhen 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.