From UML to process algebra and back : an automated approach to model-checking software design artifacts of concurrent systems

D. Remenska, J.A. Templon, T.A.C. Willemse, P. Homburg, K. Verstoep, A. Casajus, H.E. Bal

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

10 Citations (Scopus)

Abstract

One of the challenges in concurrent software development is early discovery of design errors which could lead to deadlocks or race-conditions. For safety-critical and complex distributed applications, traditional testing does not always expose such problems. Performing more rigorous formal analysis typically requires a model, which is an abstraction of the system. For object-oriented software, UML is the industry-adopted modeling language. UML offers a number of views to present the system from different perspectives. Behavioral views are necessary for the purpose of model checking, as they capture the dynamics of the system. Among them are sequence diagrams, in which the interaction between components is modeled by means of message exchanges. UML 2.x includes rich features that enable modeling code-like structures, such as loops, conditions and referring to existing interactions. We present an automatic procedure for translating UML into mCRL2 process algebra models. Our prototype is able to produce a formal model, and feed model-checking traces back into any UML modeling tool, without the user having to leave the UML domain. We argue why previous approaches of which we are aware have limitations that we overcome. We further apply our methodology on the Grid framework used to support production activities of one of the LHC experiments at CERN.
Original languageEnglish
Title of host publicationNASA Formal Methods (5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings)
EditorsG. Brat, N. Rungta, A. Venet
Place of PublicationBerlin
PublisherSpringer
Pages244-260
ISBN (Print)978-3-642-38087-7
DOIs
Publication statusPublished - 2013
Event5th NASA Formal Methods Symposium (NFM 2013), May 14-16, 2013, Moffett Field, CA, USA - NASA Ames Research Center , Moffett Field, CA, United States
Duration: 14 May 201316 May 2013
https://ti.arc.nasa.gov/events/nfm-2013/

Publication series

NameLecture Notes in Computer Science
Volume7871
ISSN (Print)0302-9743

Conference

Conference5th NASA Formal Methods Symposium (NFM 2013), May 14-16, 2013, Moffett Field, CA, USA
Abbreviated titleNFM 2013
CountryUnited States
CityMoffett Field, CA
Period14/05/1316/05/13
Internet address

Fingerprint Dive into the research topics of 'From UML to process algebra and back : an automated approach to model-checking software design artifacts of concurrent systems'. Together they form a unique fingerprint.

  • Cite this

    Remenska, D., Templon, J. A., Willemse, T. A. C., Homburg, P., Verstoep, K., Casajus, A., & Bal, H. E. (2013). From UML to process algebra and back : an automated approach to model-checking software design artifacts of concurrent systems. In G. Brat, N. Rungta, & A. Venet (Eds.), NASA Formal Methods (5th International Symposium, NFM 2013, Moffett Field, CA, USA, May 14-16, 2013. Proceedings) (pp. 244-260). (Lecture Notes in Computer Science; Vol. 7871). Springer. https://doi.org/10.1007/978-3-642-38088-4_17