We present the UMC framework for the formal analysis of concurrent systems specified by collections of UML state machines. The formal model of a system is given by a doubly labelled transition system, and the logic used to specify its properties is the state-based and event-based logic UCTL. UMC is an on-the-fly analysis framework which allows the user to interactively explore a UML model, to visualize abstract behavioural slices of it and to perform local model checking of UCTL formulae. An automotive scenario from the serviceoriented computing (SOC) domain is used as case study to illustrate our approach.
A state/event-based model-checking approach for the analysis of abstract system properties
ter Beek M H;Fantechi A;Gnesi S;Mazzanti F
2011
Abstract
We present the UMC framework for the formal analysis of concurrent systems specified by collections of UML state machines. The formal model of a system is given by a doubly labelled transition system, and the logic used to specify its properties is the state-based and event-based logic UCTL. UMC is an on-the-fly analysis framework which allows the user to interactively explore a UML model, to visualize abstract behavioural slices of it and to perform local model checking of UCTL formulae. An automotive scenario from the serviceoriented computing (SOC) domain is used as case study to illustrate our approach.File in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
prod_199409-doc_43607.pdf
solo utenti autorizzati
Descrizione: A state/event-based model-checking approach for the analysis of abstract system properties
Tipologia:
Versione Editoriale (PDF)
Dimensione
2.36 MB
Formato
Adobe PDF
|
2.36 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.