The work presented here is part of a project that aims at the definition of a methodology for developing realtime 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 realtime issues. Therefore we aim at a formalization of a suitable extension of UML statecharts. For this purpose we do not de...