Applying Model Checking to Concurrent UML Models

By: Patrice Gagnon, Farid Mokhati, Mourad Badri

Abstract

The formal and object-oriented language Maude, based on rewriting logic, supports formal specification and programming of concurrent systems, as well as model checking. We focus on UML class, state and communication diagrams. The major motivations of this work are: (1) translating concurrent UML diagrams into a Maude formal specification and (2) applying model checking to the generated specifications. The approach is illustrated using a concrete case study.

Cite as:

Patrice Gagnon, Farid Mokhati, Mourad Badri, “Applying Model Checking to Concurrent UML Models”, Journal of Object Technology, Volume 7, no. 1 (January 2008), pp. 59-84, doi:10.5381/jot.2008.7.1.a1.

PDF | HTML | DOI | BiBTeX | Tweet this | Post to CiteULike | Share on LinkedIn

The JOT Journal   |   ISSN 1660-1769   |   DOI 10.5381/jot   |   AITO   |   Open Access   |    Contact