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 specified as UML state machines. © 2011 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Hvid Hansen, H., Ketema, J., Luttik, B., Mousavi, M., Van De Pol, J., & Dos Santos, O. M. (2012). Formal Methods for Components and Objects. (B. K. Aichernig, F. S. de Boer, & M. M. Bonsangue, Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6957, pp. 225–250). Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-642-25271-6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
