In the paper we present the use of UML statecharts for the design and the specification of the dynamic behavior of a system. We show that the possible system evolutions can be formally represented as a Double Labelled Transition System and present a temporal logic which allows both to specify the basic properties that a configuration should satisfy, and to combine these basic predicates with advanced logic or temporal operators.
Mu-ACTL+: a temporal logic for UML statechart diagrams
Gnesi S;Mazzanti F
2003
Abstract
In the paper we present the use of UML statecharts for the design and the specification of the dynamic behavior of a system. We show that the possible system evolutions can be formally represented as a Double Labelled Transition System and present a temporal logic which allows both to specify the basic properties that a configuration should satisfy, and to combine these basic predicates with advanced logic or temporal operators.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_160155-doc_124216.pdf
accesso aperto
Descrizione: A temporal logic for UML Statechart diagrams
Dimensione
180.04 kB
Formato
Adobe PDF
|
180.04 kB | Adobe PDF | Visualizza/Apri |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
