The analysis of concurrent programs that create networks with arbitrary numbers of nodes is extremely complex and solutions either give imprecise answers or do not scale.
This talk presents a proof technique that we have used to analyse these programs for deriving properties such as deadlock freedom, upper bounds of resource usages and of the computational cost. The proof technique is modular and consists of two parts:
In this paper we present an algorithm for session type inference for the pi-calculus. Type inference for session types has previously been achieved by either imposing limitations and restriction on the pi-calculus, or by converting the problem to linear types, conducting type inference on the new problem, and converting the result back to session types. Our approach is based on constraint generation and solving. We generate constraints for a process based on its syntactical components, and afterwards solve the generated constraints in a predetermined order. We prove the soundness, completeness, and termination of this approach.
We address the problem of designing distributed applications which require the interaction of loosely-coupled and mutually distrusting services. In this setting, services can use contracts to protect themselves from unsafe interactions with the environment: when their partner in an interaction does not respect its contract, it can be be blamed (and punished) by the service infrastructure. We extend a core calculus for contract-oriented services, by using a semantic model of contracts which subsumes various kinds of behavioural types. In this formal framework, we study some notions of honesty for services, which measure their ability to respect contracts, under different assumptions about the environment. In particular, we find conditions under which these notions are (un)decidable.
Programmers often code up asynchronous message-passing systems as communicating finite-state actors. An actor in some state listens for messages, responds to those messages, and transitions to another state. Most of these systems allow messages to carry actor addresses.
This paper presents a kernel language for implementing and specifying such systems. A specification consists of finite-state machines, expressing what kind of messages each component should expect and what kind of actions it should take in response. In addition, a specification may prescribe how a component may use an address received from a message as well as how a component handles inputs on addresses that it sends out. Finally, a conformance relation articulates when an implementation meets such a specification.
We survey our work on choreographies and behavioural contracts in multiparty interactions. In particular theories of behavioural contracts are presented which enable reasoning about correct service composition (contract compliance) and service substitutability (contract refinement preorder) under different assumptions concerning service communication: synchronous communication with patient non-preemptable or impatient invocations, or asynchronous communication. Correspondingly, relations concerning behavioural contracts and choreographic descriptions are considered, where a contract for each communicating party is, e.g., derived by projection.
Contract refinement relations are induced as the maximal preoders which preserve contract compliance and global traces. The obtained preorders are then characterized in terms of a new form of testing, called compliance testing (where not only tests must succeed but also the system under test), and compared with classical preorders. Moreover, recent work about adaptable choreographies and behavioural contracts is presented, where the theory above is extended to update mechanisms allowing choreographies/contracts to be modified at run-time by internal (self-adaptation) or external intervention.