Today, web services are the major technology for deploying systems that make their functionality remotely accessible, discoverable, and composable, giving rise to the paradigm of service-oriented computing (SOC). To adequately model SOC systems, and to rigorously reason about their behavior, suitable formal calculi equipped with corresponding analysis techniques are required. This paper presents such a calculus called stream-based service-centered calculus (SSCC).
SSCC extends a previously introduced process calculus by a notion of streams that allows for the collection of results from ongoing computations and makes them available for new ones. Thus, SSCC becomes more suitable for modeling service composition and orchestration, while still allowing static analysis techniques. The paper first formally defines the syntax, operational semantics, and type system of SSCC; it then introduces a theory of the dynamic behavior of SSCC processes by a labeled transition system on top of which strong and weak notions of process equivalence (bisimilarity) are introduced.
A characterizing feature of this paper, however, is the extensive presentation of examples that demonstrates the practical application of SSCC. First, a simple example illustrates the main features of the calculus; later, a catalog of previously published workflow patterns is expressed; finally, two case studies from a larger automotive scenario are modeled. From these examples the need for program transformations arises, so the paper finally discusses how services modeled in an object-oriented style can be systematically transformed to a session-centered style. These efforts to make the results accessible to a wider audience make the paper exceptional reading.