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.
|Name||Lecture Notes in Computer Science|
|Conference||9th International Symposium on Formal Methods for Components and Objects, FMCO 2010|
|Period||29/11/10 → 1/12/10|
|Other||29 Nov - 01 Dec 2010|