We present a strategy for model-checking the correctness of service composition. We do so in the context of SRML, a formal modelling framework for service-oriented computing being defined within the SENSORIA project. We introduce a methodology for encoding patterns of typical service interaction with UML state machines and present a strategy for checking SRML specifications of service composition based on such patterns. For that purpose, we use the action-state branching time temporal logic UCTL and the model-checker UMC.
A model-checking approach for service component architectures
Mazzanti F;Gnesi S
2009
Abstract
We present a strategy for model-checking the correctness of service composition. We do so in the context of SRML, a formal modelling framework for service-oriented computing being defined within the SENSORIA project. We introduce a methodology for encoding patterns of typical service interaction with UML state machines and present a strategy for checking SRML specifications of service composition based on such patterns. For that purpose, we use the action-state branching time temporal logic UCTL and the model-checker UMC.File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
prod_178663-doc_13076.pdf
solo utenti autorizzati
Descrizione: A model-checking approach for service component architectures
Tipologia:
Versione Editoriale (PDF)
Dimensione
244.48 kB
Formato
Adobe PDF
|
244.48 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
