Generating Maude specifications from UML use case diagrams

Abstract

This paper presents a systematic approach supporting the translation of UML use case diagrams, describing the functional requirements of a system, into a Maude formal specification. The proposed approach also considers the static and dynamic features of object-oriented systems. The formal and object-oriented language Maude, based on rewriting logic, supports formal specification and programming of concurrent systems. The major motivations of this work are: (1) translating the functional requirements of an object-oriented system, specified using UML use case diagrams, into a Maude specification, (2) translating its static and dynamic aspects, described using UML class, communication and state-transitions diagrams respectively, into a Maude specification, and (3) integrating the formal verification of the consistency of the models, since the analysis phase. A case study is presented to illustrate our approach. © JOT, 2009.