We give a formal account of SSCC, a calculus for modeling service-based systems, suitable to describe both service composition (orchestration) and the protocols that services follow when invoked (conversation). The calculus includes primitives for defining and invoking services, for isolating conversations (called sessions) among clients and servers, and for orchestrating services. The calculus is equipped with a reduction and a labeled transition semantics related by an equivalence result. SSCC provides a good trade-off between expressive power for modeling and simplicity for analysis. We assess the expressive power by modeling van der Aalst workflow patterns and an automotive case study from the European project Sensoria. For analysis, we present a simple type system ensuring compatibility of client and service protocols. We also study the behavioral theory of the calculus, highlighting some axioms that capture the behavior of the different primitives. As a final application of the theory, we define and prove correct some program transformations. These allow to start modeling a system from a typical UML Sequence Diagram, and then transform the specification to match the service-oriented programming style, thus simplifying its implementation using web services technology.
Static analysis techniques based on session types discern concurrent programs that ensure the fidelity of protocol sessions -- for each input (output) end point of a session there is exactly an output (input) end point available -- while maintaining a good expressiveness that allows to represent the standard pi-calculus and several typing disciplines. More advanced type systems, enforcing stronger properties as deadlock-freedom or even progress, sensibly reduce the set of typed processes, thus mining the expressiveness of the analysis. Herein, we propose a first step towards a compromise solution to this problem: we develop a session based type checking algorithm that releases some deadlocks (when co-actions on the same channel occur in sequence in a thread). This procedure may help the software development process: the typing algorithm detects a deadlock, but instead of rejecting the code, fixes it by looking into the session types and producing new safe code that obeys the protocols and is deadlock-free.
We propose a process algebra, the Algebra of Behavioural Types, as a language for typing concurrent objects. A type is a higher-order labelled transition system that characterises all possible life cycles of a concurrent object. States represent interfaces of objects; state transitions model the dynamic change of object interfaces. Moreover, a type provides an internal view of the objects that inhabits it: a synchronous one, since transitions correspond to message reception. To capture this internal view of objects we define a notion of bisimulation, strong on labels and weak on silent actions. We study several algebraic laws that characterise this equivalence, and obtain completeness results for image-finite types.
We thoroughly study the behavioural theory of EPi, a pi-calculus extended with polyadic synchronisation. We show that the natural contextual equivalence, barbed congruence, coincides with early bisimilarity, which is thus its co-inductive characterisation. Moreover, we relate early bisimilarity with the other usual notions, ground, late and open, obtaining a lattice of equivalence relations that clarifies the relationship among the ``standard'' bisimilarities. Furthermore, we apply the theory developed to obtain an expressiveness result: EPi extended with key encryption primitives may be fully abstractly encoded in the original EPi calculus. The proposed encoding is sound and complete with respect to barbed congruence; hence, cryptographic EPi (CEPi) gets behavioural theory for free, what contrasts with other process languages with cryptographic constructs that usually require a big effort to develop such theory. Therefore, it is thus possible to use CEPi to analyse and to verify properties of security protocols using equational reasoning. To illustrate this claim, we prove the symmetric and asymmetric cryptographic system laws, and the correctness of a protocol of secure message exchange.
This chapter presents the behavioural theory of some of the Sensoria core calculi. We consider SSCC, muse and CC as representatives of the session-based approach and COWS as representative of the correlation-based one. For SSCC, muse and CC the main point is the structure that the session/conversation mechanism creates in programs. We show how the differences between binary sessions, multiparty sessions and dynamic conversations are captured by different behavioural laws. We also exploit those laws for proving the correctness of program transformations. For COWS the main point is that communication is prioritised (the best matching input captures the output), and this has a strong influence on the behavioural theory of COWS. In particular, we show that communication in COWS is neither purely synchronous nor purely asynchronous.
Languages and models for service oriented applications usually include primitives and constructs for exception and compensation handling. Exception handling is used to react to unexpected events while compensation handling is used to undo previously completed activities. In this chapter we investigate the impact of exception and compensation handling in message-based process calculi and the related theories developed within Sensoria.
We propose a general type notation, formal semantics and a sound, compositional, and decidable type system to characterise some liveness properties of distributed systems. In the context of mobile processes, we define two concepts, activeness (ability to send/receive on a channel) and responsiveness (ability to reliably conduct a conversation on a channel), that make the above properties precise. The type system respects the semantic definitions of the concepts, in the sense that the logical statements it outputs are, according to the semantics, correct descriptions of the analysed process. Our work is novel in two aspects. First, since mobile processes can make and communicate choices, a fundamental component of data representation (where a piece of data matches one of a set of patterns) or conversations (where the protocol may permit more than one message at each point), our types and type system use branching and selection to capture activeness and responsiveness in process constructs necessary for such usage patterns. Secondly, conditional properties offer compositionality features that permit analysing components of a system individually, and indicate, when applicable, what should be provided to the given process before the properties hold.
Session types allow communication protocols to be specified type-theoretically so that protocol implementations can be verified by static type-checking. We extend previous work on session types for distributed object-oriented languages in three ways. (1) We attach a session type to a class definition, to specify the possible sequences of method calls. (2) We allow a session type (protocol) implementation to be modularized, i.e., partitioned into separately-callable methods. (3) We treat session-typed communication channels as objects, integrating their session types with the session types of classes. The result is an elegant unification of communication channels and their session types, distributed object-oriented programming, and a form of typestates supporting non-uniform objects, i.e., objects that dynamically change the set of available methods. We define syntax, operational semantics, a sound type system, and a correct and complete type checking algorithm for a small distributed class-based object-oriented language. Static typing guarantees that both sequences of messages on channels, and sequences of method calls on objects, conform to type-theoretic specifications, thus ensuring type-safety. The language includes expected features of session types, such as delegation, and expected features of object-oriented programming, such as encapsulation of local state. We also describe a prototype implementation as an extension of Java.
We define a small class-based object-oriented language in which the
availability of methods depends on an object's abstract state:
objects' interfaces are dynamic. Each class has a session
type which provides a global specification of the availability of
methods in each state. A key feature is that the abstract state of an
object may depend on the result of a method whose return type is an
enumeration. Static typing guarantees that methods are only called
when they are available. We present both a type system, in
which the typing of a method specifies pre- and post-conditions for
its object's state, and a typechecking algorithm, which
infers the pre- and post-conditions from the session type, and prove
type safety results. Inheritance is included; a subtyping relation on
session types, related to that found in previous literature,
characterizes the relationship between method availability in a
subclass and in its superclass. We illustrate the language and its
type system with example based on a Java-style iterator and a
hierarchy of classes for accessing files, and conclude by outlining
several ways in which our theory can be extended towards more
practical languages.
Keywords: Static typing, session types, non-uniform method
availability, inheritance.
Most business applications rely on the notion of long running transaction as a fundamental building block. This paper presents a calculus for modelling long running transactions within the framework of the pi-calculus, with support for compensation as a recovery mechanism. The underlying model of this calculus is the asynchronous polyadic pi-calculus, with transaction scopes and dynamic installation of compensation processes. We add to the framework a type system which guarantees that transactions are unequivocally identified, ensuring that upon a failure the correct compensation process is invoked. Moreover, the operational semantics of the calculus ensures both installation and activation of the compensation of a transaction.
We analyse the relationship between object-oriented modelling and session-based, service-oriented modelling, starting from a typical UML Sequence Diagram and providing a program transformation into a service-oriented model. We also provide a similar transformation from session-based specifications into request-response specifications. All transformations are specified in SSCC---a process calculus for modelling and analysing service-oriented systems---and proved correct with respect to a suitable form of behavioural equivalence (full weak bisimilarity). Since the equivalence is proved to be compositional, results remain valid in arbitrary contexts.
We give a formal account of a calculus for modeling service-based systems, suitable to describe both service composition (orchestration) and the protocol that services run when invoked (conversation). The calculus includes primitives for defining and invoking services, for isolating conversations between clients and servers, and for orchestrating services. The calculus is equipped with a reduction and a labeled transition semantics related by an equivalence result. To hint how the structuring mechanisms of the language can be exploited for static analysis we present a simple type system guaranteeing the compatibility between client and server protocols, an application of bisimilarity to prove equivalence among services, and we discuss deadlock-avoidance.
We seek for a small set of primitives that might serve as a basis for formalising and programming service oriented applications over global computers. As an outcome of this study we introduce here SCC, a process calculus that features explicit notions of service definition, service invocation and session handling. Our proposal has been influenced by Orc, a programming model for structured orchestration of services, but the SCC's session handling mechanism allows for the definition of structured interaction protocols, more complex than the basic request-response provided by Orc. We present syntax and operational semantics of SCC and a number of simple but nontrivial programming examples that demonstrate flexibility of the chosen set of primitives. A few encodings are also provided to relate our proposal with existing ones.
This paper describes a proposal for typing the behavior of objects in component models. Most component models, CORBA in particular, do not offer any support for expressing behavior al properties of objects beyond the ``static'' information provided by IDLs We build on the works by Honda et al. and Gay and Hole to show how session types can be effectively used for describing protocols, extending the information currently provided by object interfaces. We show how session types not only allow high level specifications of complex object interactions, but also allow the definition of powerful interoperability tests at the protocol level, namely compatibility and substitutability of objects
We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static typechecking. A session type, associated with a communication channel, specifies the state transitions of a protocol and also the data types of messages associated with transitions; thus typechecking can verify both correctness of individual messages and correctness of sequences of transitions. Previously, session types have mainly been studied in the context of the pi-calculus; instead, our formulation is based on a multi-threaded functional language with side-effecting input/output operations. Our typing judgements statically describe dynamic changes in the types of channels, and our function types not only specify argument and result types but also describe changes in channels. We formalize the syntax, semantics and type checking system of our language, and prove subject reduction and runtime type safety theorems.
2005
2004
Session Types for Functional Multithreading
We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static typechecking. A session type, associated with a communication channel, specifies the state transitions of a protocol and also the data types of messages associated with transitions; thus typechecking can verify both correctness of individual messages and correctness of sequences of transitions. Previously session types have mainly been studied in the context of the pi-calculus; instead, our formulation is based on a multi-threaded functional language with side-e ecting input/output operations. Our typing judgements statically describe dynamic changes in the types of channels, our channel types statically track aliasing, and our function types not only specify argument and result types but also describe changes in channels. We formalize the syntax, semantics and typing rules of our language, and prove subject reduction and runtime type safety theorems.
This paper presents a type system to control the migration of code between sites in a concurrent distributed framework. The type system constitutes a decidable mechanism to ensure specific security policies, which control remote communication, process migration, and channel creation. The approach is as follows: each network administrator specifies sites privileges, and a type system checks that the processes running at those sites, as well as the composition of the sites, respect these policies. At runtime, well-typed networks do not violate the security policies declared for each site.
We define a lexically scoped, asynchronous and distributed pi-calculus with local communication and process migration. This calculus adopts the network-awareness principle for distributed programming and follows a simples model of distribution for mobile calculi: a lexical scoping discipline combines static scoping with dynamic linking, associating channels to a fixed site throughout computation. Furthermore, it provides for both remote invocation and process migration. A simple equivalence law captures the essence of the model: a process behaviour depends on the names it uses, not where it runs.
Concurrent objects may offer services non-uniformly, constraining the acceptance of messages on the states of objects. We advocate a looser view of communication errors. Safe programmes must guarantee that every message has a chance of being received if it requests a method that may become enabled at some point in the future. We formalise non-uniform concurrent objects in TyCO, a name-passing object calculus, and ensure program safety via a type system. Types are terms of a process algebra that describes dynamic aspects of the behaviour of objects.
We present an undecidability proof of the notion of communication errors in the polyadic pi-calculus. The demonstration follows a general pattern of undecidability proofs---reducing a well-known undecidable problem to the problem in question. We make use of an encoding of the lambda-calculus into the pi-calculus to show that the decidability of communication errors would solve the problem of deciding whether a lambda term has a normal form.