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.

Model Checking UML Specifications of Real-Time Software

LAVAZZA, LUIGI ANTONIO;MAURI, MARCO
2002-01-01

Abstract

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.
Proceedings of the Eighth International Conference on Engineering of Complex Computer Systems
9780769517575
The 8th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2002)
Greenbelt, Maryland
2–4 December, 2002
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11383/17575
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 16
  • ???jsp.display-item.citation.isi??? 5
social impact