Automated Verification of Executable UML Models

Hansen, Helle Hvid and Ketema, Jeroen and Luttik, Bas and Mousavi, MohammadReza and Pol van de, Jaco 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.

PDF
Restricted to UT campus only: Request a copy
543Kb

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
Faculty:	Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:	Formal Methods and Tools (FMT)
Link to this item:	http://purl.utwente.nl/publications/79011
Official URL:	http://dx.doi.org/10.1007/978-3-642-25271-6_12
Export this item as:	BibTeX EndNote HTML Citation Reference Manager

Show download statistics for this publication

Repository Staff Only: item control page