Cím | Automated Formal Verification of Model Transformations |
Közlemény típusa | Conference Paper |
Kiadás éve | 2003 |
Szerzők | Varró, D., and Pataricza, A. |
Szerkesztő | Jürjens, J., Rumpe, B., France, R., and Fernandez, E. B. |
Konferencia neve | CSDUML 2003: Critical Systems Development in UML; Proceedings of the UML'03 Workshop |
Kiadás dátuma | September |
Kiadó | Technische Universität München |
Összefoglalás | When 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. |
URL | http://www.inf.mit.bme.hu/FTSRG/Publications/varro/2003/csduml2003_vp.pdf |