Model Checking UML Specifications of Real-Time Software

UML is being increasingly used to model real-timesoftware. On one hand this is reasonable, since UML isvery popular and relatively easy to use. On the otherhand, the semantics of UML is not well defined, thus UMLdoes not support formal analysis, which is needed toprove properties like safety, utility, liveness, etc. Thisarticle describes a way to make UML models formallyverifiable. The presented approach is made possible byextending UML in order to represent time-dependentinformation and time constraints, and by formalizing theresulting language. The formalization is achieved bymapping UML state diagrams to Timed Statecharts. UMLstate models are translated into timed automata, so thatthe model checking tool Kronos can be employed to verifytime-dependent properties. A central issue of the workpresented here is that developers can take advantage ofthe formal methods being employed while skipping thecomplex and expensive formal modeling phase.