@article{GOO06d,
title = { Validating Timed {UML} models by simulation and verification },
author = {Graf, Susanne and Ober, Ileana and Ober, Iulian},
month = {apr},
year = {2006},
journal = {STTT, Software Tools for Technology Transfer},
number = {2},
volume = {8},
team = {DCS},
abstract = {This paper presents a technique and a tool for model-checking operational (design level) UML models based on a mapping to a model of communicating extended timed automata. The target language of the mapping is the IF format, for which existing model-checking and simulation tools can be used. Our approach takes into consideration most of the structural and behavioral features of UML, including object-oriented aspects. It handles the combination of operations, state machines, inheritance and polymorphism, with a particular semantic profile for communication and concurrency. We adopt a UML profile that includes extensions for expressing timing. The breadth of concepts covered by our mapping is an important point, as many previous approaches for applying formal validation to UML put stronger limiting conditions on the input models. For expressing properties about models, a formalism called <i>UML observers</i> is defined in this paper. Observers reuse existing concepts like classes and state machines, and they may express a significant class of linear temporal properties. },
}
