Model checking of UML models via a mapping to communicating extended timed automata

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