Applying Model Checking to Concurrent UML Models.
Patrice Gagnon, Farid Mokhati, Mourad Badri · The Journal of Object Technology · 2008
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.