Timed-automata semantics and analysis of UML/SPT models with coneurrency

UML can be effectively used for the design and analysis of real-time systems. UML profiles for real-time, like the current OMG's standard UML/SPT enable the modeling of quantitative requirements such as time constraints as well as behavioral features such as concurrency. Because of the multitude of diagrams and their complexity, UML/SPT models face the challenging issue of consistency. In this paper we look into the behavioral consistency and particularly into concurrency-related properties of UML/SPT models. In order to do so, we formally define the UML/SPT concurrency domain model in terms of timed automata. As a straightforward application of this semantics, UML/SPT concurrent models can be validated using well-established model checking techniques and tools.