Model checking UML specifications of real time software

UML is being increasingly used to model real-time software. On one hand this is reasonable, since UML is very popular and relatively easy to use. On the other hand, the semantics of UML is not well defined, thus UML does not support formal analysis, which is needed to prove properties like safety, utility, liveness, etc. This article describes a way to make UML models formally verifiable. The presented approach is made possible by extending UML in order to represent time-dependent information and time constraints, and by formalizing the resulting language. The formalization is achieved by mapping UML state diagrams to Timed Statecharts. UML state models are translated into timed automata, so that the model checking tool Kronos can be employed to verify time-dependent properties. A central issue of the work presented here is that developers can take advantage of the formal methods being employed while skipping the complex and expensive formal modeling phase.