Applying Model Checking to Concurrent UML Models
By: Patrice Gagnon, Farid Mokhati, Mourad Badri
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.