A Formalization of UML Statecharts for Real-Time Software Modeling

The work presented here is part of a project that aims at the definition of a methodology for developing real-time software systems based on UML. In fact, being relatively easy to learn and use, UML is very popular, unlike formal methods. However, formal models provide developers with several benefits: they can be used for activities –like property verification, simulation, test case generation, etc.– which are vital for the development of real-time software. Such activities are more difficult, more error-prone or less effective when carried out on UML models, because UML is not formally defined. In this paper we explore the possibility to formalize the part of UML that is more important for the specification of real-time behavior, namely the statecharts. Actually, previous experiences indicated that UML statecharts have to be extended in order to cope with real-time issues. Therefore we aim at a formalization of a suitable extension of UML statecharts. For this purpose we do not develop a new formalism, instead we exploit the Timed Statecharts formalism proposed by Kesten and Pnueli. The contributions of the paper are: the evaluation of the difference between Timed Statecharts and UML (properly extended for modeling real-time issues), a mapping of extended UML statecharts to Timed Statecharts, the application of the proposed approach to a case study