Automated Verification of Executable UML Models

Helle Hvid Hansen; J. Ketema; Bas Luttik; MohammadReza Mousavi; Jan Cornelis van de Pol; Oscar Marchi dos Santos

doi:10.1007/978-3-642-25271-6_12

Automated Verification of Executable UML Models

Helle Hvid Hansen
, J. Ketema
, Bas Luttik
, MohammadReza Mousavi
, Jan Cornelis van de Pol
, Oscar Marchi dos Santos

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

15 Citations (Scopus)

13 Downloads (Pure)

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.

Original language	Undefined
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
Publisher	Springer
Pages	225-250
Number of pages	26
ISBN (Print)	978-3-642-25270-9
DOIs	https://doi.org/10.1007/978-3-642-25271-6_12
Publication status	Published - Nov 2011
Event	9th International Symposium on Formal Methods for Components and Objects, FMCO 2010 - Graz, Austria Duration: 29 Nov 2010 → 1 Dec 2010

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	6957
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

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

Keywords

METIS-284928
EWI-21051
IR-79011

Access to Document

10.1007/978-3-642-25271-6_12

http://eprints.eemcs.utwente.nl/secure2/21051/01/fmco-2010.pdf

Cite this

Hansen, H. H., Ketema, J., Luttik, B., Mousavi, M., van de Pol, J. C., & Marchi dos Santos, O. (2011). Automated Verification of Executable UML Models. In Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers (pp. 225-250). (Lecture Notes in Computer Science; Vol. 6957). Springer. https://doi.org/10.1007/978-3-642-25271-6_12

@inproceedings{45fe3b8a5eba462f8fd8228fe828a7c7,

title = "Automated Verification of Executable UML Models",

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.",

keywords = "METIS-284928, EWI-21051, IR-79011",

author = "Hansen, \{Helle Hvid\} and J. Ketema and Bas Luttik and MohammadReza Mousavi and \{van de Pol\}, \{Jan Cornelis\} and \{Marchi dos Santos\}, Oscar",

note = "eemcs-eprint-21051 ; 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010 ; Conference date: 29-11-2010 Through 01-12-2010",

year = "2011",

month = nov,

doi = "10.1007/978-3-642-25271-6\_12",

language = "Undefined",

isbn = "978-3-642-25270-9",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "225--250",

booktitle = "Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers",

address = "Germany",

}

Hansen, HH, Ketema, J, Luttik, B, Mousavi, M, van de Pol, JC & Marchi dos Santos, O 2011, Automated Verification of Executable UML Models. in Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers. Lecture Notes in Computer Science, vol. 6957, Springer, Berlin, pp. 225-250, 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010, 29/11/10. https://doi.org/10.1007/978-3-642-25271-6_12

Automated Verification of Executable UML Models. / Hansen, Helle Hvid; Ketema, J.; Luttik, Bas et al.
Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers. Berlin: Springer, 2011. p. 225-250 (Lecture Notes in Computer Science; Vol. 6957).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Automated Verification of Executable UML Models

AU - Hansen, Helle Hvid

AU - Ketema, J.

AU - Luttik, Bas

AU - Mousavi, MohammadReza

AU - van de Pol, Jan Cornelis

AU - Marchi dos Santos, Oscar

N1 - eemcs-eprint-21051

PY - 2011/11

Y1 - 2011/11

N2 - 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.

AB - 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.

KW - METIS-284928

KW - EWI-21051

KW - IR-79011

U2 - 10.1007/978-3-642-25271-6_12

DO - 10.1007/978-3-642-25271-6_12

M3 - Conference contribution

SN - 978-3-642-25270-9

T3 - Lecture Notes in Computer Science

SP - 225

EP - 250

BT - Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers

PB - Springer

CY - Berlin

T2 - 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010

Y2 - 29 November 2010 through 1 December 2010

ER -