Automated Verification of Executable UML Models


Hansen, Helle Hvid and Ketema, Jeroen and Luttik, Bas and Mousavi, MohammadReza and Pol, Jaco van de and Marchi dos Santos, Oscar (2011) Automated Verification of Executable UML Models. In: 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010, 29 Nov - 01 Dec 2010, Graz, Austria (pp. pp. 225-250).

[img] PDF
Restricted to UT campus only
: Request a copy
Abstract: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 specied as UML state machines.
Item Type:Conference or Workshop Item
Copyright:© 2011 Springer
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:
Official URL:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page