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

Formal design methods, that might serve as a basis for spec- ifying and analyzing abstract models of service orchestra- tions, 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 se- mantic framework for UML4SOA models of service-oriented systems. The UML4SOA language is a UML profile de- veloped in the EU SENSORIA project for modeling services behavior focusing on service orchestration aspects. We com- plement the graphical model of a service orchestration sce- nario with a formal description that is suitable for rigorous execution-platform-independent analysis. We map the be- havioral primitives of UML4SOA activity diagrams into a particular class of Abstract State Machines (ASMs) able to model notions of service interactions and orchestrations. Copyright 2010 ACM.