Validation of UML Models via a Mapping to Communicating Extended Timed Automata

Abstract. We present a technique and a tool for model-checking operational UML models based on a mapping of object oriented UML models into a framework of communicating extended timed automata- in the IF format- and the use of the existing model-checking and simulation tools for this format. We take into account most of the structural and behavioral characteristics of classes and their interplay and tackle issues like the combination of operations, state machines, inheritance and polymorphism, with a particular semantic profile for communication and concurrency. The UML dialect considered here, also includes a set of extensions for expressing timing. Our approach is implemented by a tool importing UML models via an XMI repository, and thus supporting several commercial and noncommercial UML editors. For user friendly interactive simulation, an interface has been built, presenting feedback to the user in terms of the original UML model. Model-checking and model exploration can be done by reusing the existing IF state-of-the-art validation environment.