A Model of Service-Oriented Architectures

Architectural styles and patterns play an important role in software engineering. Over the last years, a new style based on the notion of services emerged, which we call the service-oriented architecture style. However, this style is usually only stated informally, which may cause inherent problems such as ambiguity, wrong conclusions, and the difficulty of checking the conformance of a system to the style. We address these problems by providing a formal, denotational semantics of the service-oriented architecture style and two variants thereof: the layered architecture style and the strict architecture style. Loosely speaking, in our model of the service-oriented architecture style, services are a means of communication. Components exchange services between each other via ports. The layered architecture variant imposes a well-foundedness constraint on the communication structure, while the strict variant imposes an antitransitivity constraint. We analyze the notions of syntactic and semantic dependencies for service-oriented architectures and investigate their relationship. Moreover, the expected informal properties of the styles are formulated as theorems. Finally, we present a method for soundly analyzing instances of the style. Our rigorous approach enables building higher-quality architectures, for which properties can be mathematically stated and proven, by enforcing formal discipline on the inter-component scale.