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.

• Type: Journal
• Year: 2008
• Where: JOT
• Authors: Patrice Gagnon, Farid Mokhati, Mourad Badri
• Keywords: Concurrent Uml, Concurrent Uml Models, Formal Specification, JOT 2008