| Title | Automated Formal Verification of Model Transformations |
| Publication Type | Conference Paper |
| Year of Publication | 2003 |
| Authors | Varró, D., and Pataricza, A. |
| Editor | Jürjens, J., Rumpe, B., France, R., and Fernandez, E. B. |
| Conference Name | CSDUML 2003: Critical Systems Development in UML; Proceedings of the UML'03 Workshop |
| Date Published | September |
| Publisher | Technische Universität München |
| Abstract | 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 |
