A Model-Checking Approach for Service Component Architectures

12 years 7 months ago
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
João Abreu, Franco Mazzanti, José Lu
Added 17 Feb 2011
Updated 17 Feb 2011
Type Journal
Year 2009
Authors João Abreu, Franco Mazzanti, José Luiz Fiadeiro, Stefania Gnesi
Comments (0)