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

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.
9780769517575
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: http://hdl.handle.net/11383/17575
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 16
  • ???jsp.display-item.citation.isi??? 5
social impact