Specifying formal executable behavioral models for structural models of service-oriented components

This paper presents a behavioral formalism based on the Abstract State Machine (ASM) formal method and intended for high-level, platform-independent, executable specification of Service-oriented Components. We complement the recent Service Component Architecture - a graphical notation able to provide the overall and the components structure - with an ASM-based formalism able to describe the workflow of the service orchestration and the services internal behavior. The resulting service-oriented component model provides an ASM-based representation of both the structural and behavioral aspects of service-oriented systems, like service interactions, service orchestration, service tasks and compensation. The ASM formal description of a service-oriented system is suitable for rigorous execution-platform-independent analysis.