| 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 |
