|
|
|
|
Model Checking UML Specifications of Real Time Software Vieri Del Bianco, Luigi Lavazza, Marco Mauri
CEFRIEL Abstract 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, being the semantics of UML not well defined, it 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 formalisation 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 modelling phase. Keywords: Real-time software, formal methods, model-checking, UML.
postscript text (385 KB) © Copyright notice Note: after the publication, we found some marginal errors in the automata descrfibed in the paper. Such errors have been corrected in the slides (164 KB) of the presentation.
|
