A Strict-Observational Interface Theory for Analysing Service Orchestrations

Service oriented computing is an accepted architectural style for developing large, distributed software systems. A particular promise of such architectures is service orchestration, i.e. the ability to combine existing services to create more complex functionality, thereby yielding new services. In this paper, we discuss application-level protocol compliance checking of service orchestrations and service protocols using the semantic domain of modal input/output automata (MIOs). Based on a practical example, we motivate and introduce new notions of refinement and compatibility, and prove that they constitute a valid interface theory. With this domain-specific interface theory, we provide a framework for application-level analysis of service orchestrations, thus complementing existing work on compatibility analysis. Our theory is tool-supported through the MIO Workbench, a verification tool for modal input/output automata.