A Model-Checking Approach for Service Component Architectures

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. 1 Specifying Service Composition with SRML The SENSORIA Reference Modelling Language (SRML) [3,5] is a domain specific language for service-oriented architectures, inspired by the Service Component Architecture [8]. SRML provides primitives for modelling composite services whose business logic involves the orchestration of interactions among elementary components and the invocation of services provided by external parties. Fig.1 is an example of a service module

• Type: Journal
• Year: 2009
• Where: FORTE
• Authors: João Abreu, Franco Mazzanti, José Luiz Fiadeiro, Stefania Gnesi
• Keywords: External Services, Formal Methods, FORTE 2009, Service Composition, Service Module