Sciweavers

Share
JOT
2008

Applying Model Checking to Concurrent UML Models

8 years 10 months ago
Applying Model Checking to Concurrent UML Models
We present, in this paper, a framework supporting a formal verification of concurrent UML models using the Maude language. We consider both static and dynamic features of concurrent object-oriented systems. We focus on UML class, state and communication diagrams. The formal and object-oriented language Maude, based on rewriting logic, supports formal specification and programming of concurrent systems, as well as model checking. 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.
Patrice Gagnon, Farid Mokhati, Mourad Badri
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where JOT
Authors Patrice Gagnon, Farid Mokhati, Mourad Badri
Comments (0)
books