A Translation of UML Components into Formal Specifications

Abstract. UML demonstrated that it is a well-suited approach to analyse and design complex systems such as industrial ones. To improve software reliability and reusability the use of formal specification is necessary but it may be difficult. There is a general lack in the formal specification of the UML concepts. This decreases the ability to develop tools and guidelines to help the specifier. Soft-ware tools are needed to assist the formal specification process, but also to prove or to verify some parts. In this paper we propose a method to formally specify concurrent and communicating components with data in UML. The principle is, first to complete the design with axioms, second to translate the diagrams into al-gebraic specifications of data types thanks to our translation tool. We describe the translation principles which are based on previous work around symbolic transi-tion systems and algebraic specifications. Finally, we sketch the implementation of our translation tool using XMI files and the XML4J parser.