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.
Citation:
Abdelouahed Gherbi, Ferhat Khendek, "Timed-Automata Semantics and Analysis of UML/SPT Models with Concurrency," isorc, pp.412-419, 10th IEEE International Symposium on Object and Component-Oriented Real-Time Distributed Computing (ISORC'07), 2007