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.
|Title of host publication||Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers|
|Place of Publication||Berlin|
|Number of pages||26|
|Publication status||Published - Nov 2011|
|Name||Lecture Notes in Computer Science|