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 proceedingConference contributionAcademicpeer-review

10 Citations (Scopus)

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 languageUndefined
Title of host publicationProceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers
Place of PublicationBerlin
PublisherSpringer
Pages225-250
Number of pages26
ISBN (Print)978-3-642-25270-9
DOIs
Publication statusPublished - Nov 2011

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume6957
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • METIS-284928
  • EWI-21051
  • IR-79011

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). Berlin: Springer. https://doi.org/10.1007/978-3-642-25271-6_12
Hansen, Helle Hvid ; Ketema, J. ; Luttik, Bas ; Mousavi, MohammadReza ; van de Pol, Jan Cornelis ; Marchi dos Santos, Oscar. / Automated Verification of Executable UML Models. Proceedings of the 9th International Symposium on Formal Methods for Components and Objects, FMCO 2010. Revised Papers. Berlin : Springer, 2011. pp. 225-250 (Lecture Notes in Computer Science).
@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",
year = "2011",
month = "11",
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",

}

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. https://doi.org/10.1007/978-3-642-25271-6_12

Automated Verification of Executable UML Models. / Hansen, Helle Hvid; Ketema, J.; Luttik, Bas; Mousavi, MohammadReza; van de Pol, Jan Cornelis; Marchi dos Santos, Oscar.

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 proceedingConference contributionAcademicpeer-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

ER -

Hansen HH, Ketema J, Luttik B, Mousavi M, van de Pol JC, Marchi dos Santos O. Automated Verification of Executable UML Models. In 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). https://doi.org/10.1007/978-3-642-25271-6_12