Helle Hvid Hansen, Jeroen Ketema, Bas Luttik, MohammadReza Mousavi and Jaco van de Pol., Post-Proceedings of the International Symposium on Formal Methods for Components and Objects (FMCO 2010), Graz, Austria, volume 6957 of Lecture Notes in Computer, Springer-Verlag, 2011.
We present a fully automated approach to verifying safety properties of Executable UML models (xUML). Our tool chain consists of a model transformation program which translates xUML models to the process algebra mCRL2, followed by symbolic model checking using LTSmin. If a safety violation is found, an error trace is visualised as a UML sequence diagram. As a novel feature, our approach allows safety properties to be specified as UML state machines.
(Paper in .pdf format)
@InProceedings{MousaviFMCO2010,
author = "Hansen, Helle Hvid and Ketema, Jeroen and Luttik, Bas and Mousavi, MohammadReza and van de Pol, Jaco",
title = "Automated Verification of Executable {UML} Models",
booktitle = "Post-Proceedings of the International Symposium on Formal Methods for Components and Objects ({FMCO} 2010)",
series = "Lecture Notes in Computer Science",
volume = "6957",
address = "Graz, Austeria",
publisher = "Springer-Verlag",
year = "2011"
}