Automated Verification of Executable UML Models


Share/Save/Bookmark

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
556kB
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:
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

 

Repository Staff Only: item control page