An ASM-based executable formal model of service-oriented component interactions and orchestration

摘要

Formal design methods, that might serve as a basis for specifying and analyzing abstract models of service orchestrations, are needed to complement the wide range of domain-specific languages (mainly based on graphical notations) that are currently being defined for engineering service-oriented systems. This paper presents a formal and executable semantic framework for UML4SOA models of service-oriented systems. The UML4S0A language is a UML profile developed in the EU SENSORIA project for modeling services behavior focusing on service orchestration aspects. We complement the graphical model of a service orchestration scenario with a formal description that is suitable for rigorous execution-platform-independent analysis. We map the behavioral primitives of UML4SOA activity diagrams into a particular class of Abstract State Machines (ASMs) able to model notions of service interactions and orchestrations.