Publication Date:
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.
Iris type:
04.01 Contributo in Atti di convegno
Keywords:
Formal modelling framework for service-oriented computing - SRML; Branching time temporal logic UCTL; model-checker UMC
List of contributors:
Gnesi, Stefania; Mazzanti, Franco
Book title:
Formal Techniques for Distributed Systems Joint 11th IFIP WG 6.1 International Conference FMOODS 2009 and 29th IFIP WG 6.1 International Conference FORTE 2009, Lisboa, Portugal, June 9-12, 2009. Proceedings