A concurrent system is a computer system with components that run in parallel and interact with each other. Such systems are ubiquitous and are notably responsible for supporting the infrastructure for transport, commerce and entertainment. They are very difficult to design and implement correctly: many different modeling languages and verification techniques have been devised to reason about them and verifying their correctness. However, existing languages and techniques can only express a limited range of systems and properties. In this dissertation, we address some of the shortcomings of established models and theories in four ways: by introducing a general modal logic, extending a modelling language with types and a more general operation, providing an automated tool support, and adapting an established behavioural type theory to specify and verify systems with unreliable communication. A modal logic for transition systems is a way of specifying properties of concurrent system abstractly. We have developed a modal logic for nominal transition systems. Such systems are common and include the pi-calculus and psi-calculi. The logic is adequate for many process calculi with regard to their behavioural equivalence even for those that no logic has been considered, for example, CCS, the pi-calculus, psi-calculi, the spi-calculus, and the fusion calculus. The psi-calculi framework is a parametric process calculi framework that subsumes many existing process calculi. We extend psi-calculi with a type system, called sorts, and a more general notion of pattern matching in an input process. This gives additional expressive power allowing us to capture directly even more process calculi than was previously possible. We have reestablished the main results of psi-calculi to show that the extensions are consistent. We have developed a tool that is based on the psi-calculi, called the psi-calculi workbench. It provides automation for executing the psi-calculi processes and generating a witness for a behavioural equivalence between processes. The tool can be used both as a library and as an interactive application. Lastly, we developed a process calculus for unreliable broadcast systems and equipped it with a binary session type system. The process calculus captures the operations of scatter and gather in wireless sensor and ad-hoc networks. The type system enjoys the usual property of subject reduction, meaning that well-typed processes reduce to well-typed processes. To cope with unreliability, we also introduce a notion of process recovery that does not involve communication. This is the first session type system for a model with unreliable communication.

Programs are more distributed and concurrent today than ever before, and structural communications are at the core. Constructing and debugging such programs are hard due to the lack of formal specifications and verifications of concurrency. Recent advances in type systems allow us to specify the structures of communications as session types, thus enabling static type checking of the usages of communication channels against protocols. The soundness of session type systems implies communication fidelity and absence of deadlock. This work proposes to formalize multiparty dependent session types as an expressive and practical type discipline for enforcing communication protocols. The type system is formulated in the setting of multi-threaded λ-calculus with inspirations from multirole logic. It is sound, and it provides linearity and coherence guarantees entirely statically. The type system supports recursion and polymorphism. The formulation is particularly suitable for practical implementation, and this work provides such a runtime implementation.

Service-oriented computing is a popular technology that facilitates the development of large-scale distributed systems. However, the modular composition and flexible coordination of such applications still remains challenging for the following reasons: 1) the services are provided as loosely coupled black boxes that only expose their interfaces to the environment; 2) interacting services are not usually known in advance: web services are dynamically chosen to fulfil certain roles and are often replaced by services with a similar functionality; 3) the nature of the service-based application is decentralised. Loose coupling of web services is often lost when it comes to the construction of an application from services. The reason is that the object-oriented paradigm, which is widely used in the implementation of web services, does not provide a mechanism for service interface self-tuning. As a result, it negatively impacts upon the interoperability of web services. In this dissertation we present a formal method for automatic service configuration in the presence of subtyping, polymorphism, and flow inheritance. This is a challenging problem. On the one hand, the interface description language must be flexible enough to maintain service compatibility in various contexts without any modification to the service itself. On the other hand, the composition of interfaces in a distributed environment must be provably consistent. Our method is based on constraint satisfaction and Boolean satisfiability. First, we define a language for specifying service interfaces in a generic form, which is compatible with a variety of contexts. The language provides support for parametric polymorphism, Boolean variables, which are used to control dependencies between any elements of interface collections, and flow inheritance using extensible records and variants. We implemented the method as a constraint satisfaction solver. In addition to this, we present a protocol for interface configuration. It specifies a sequence of steps that leads to the generation of context-specific service libraries from generic services. Furthermore, we developed a toolchain that performs a complete interface configuration for services written in C++. We integrated support for flexible interface objects (i.e. objects that can be transferred in the application along with their structural description). Although the protocol relies solely on interfaces and does not take behaviour concerns into account, it is capable of finding discrepancies between input and output interfaces for simple stateful services, which only perform message synchronisation. Two running examples (a three buyers use-case and an image processing application) are used along the way to illustrate our approach. Our results seem to be useful for service providers that run their services in the cloud. The reason is twofold. Firstly, interfaces and the code behind them can be generic as long as they are sufficiently configurable. No communication between service designers is necessary in order to ensure consistency in the design. Instead, the interface correspondence in the application is ensured by the constraint satisfaction algorithm, which we have already designed. Secondly, the configuration and compilation of every service are separated from the rest of the application. This prevents source code leaks in proprietary software which is running in the cloud.

Modern software systems, in particular distributed ones, are everywhere around us and are at the basis of our everyday activities. Hence, guaranteeing their correctness, consistency and safety is of paramount importance. Their complexity makes the verification of such properties a very challenging task. It is natural to expect that these systems are reliable and above all usable. i) In order to be reliable, compositional models of software systems need to account for consistent dynamic reconfiguration, i.e., changing at runtime the communication patterns of a program. ii) In order to be useful, compositional models of software systems need to account for interaction, which can be seen as communication patterns among components which collaborate together to achieve a common task. The aim of the Ph.D. was to develop powerful techniques based on formal methods for the verification of correctness, consistency and safety properties related to dynamic reconfiguration and communication in complex distributed systems. In particular, static analysis techniques based on types and type systems appeared to be an adequate methodology, considering their success in guaranteeing not only basic safety properties, but also more sophisticated ones like, deadlock or livelock freedom in a concurrent setting. The main contributions of this dissertation are twofold. i) On the components side: we design types and a type system for a concurrent object-oriented calculus to statically ensure consistency of dynamic reconfigurations related to modifications of communication patterns in a program during execution time. ii) On the communication side: we study advanced safety properties related to communication in complex distributed systems like deadlock-freedom, livelock-freedom and progress. Most importantly, we exploit an encoding of types and terms of a typical distributed language, session π-calculus, into the standard typed π-calculus, in order to understand the expressive power of concurrent calculi with structured communication primitives and how they stand with respect to the standard typed concurrent calculi, namely (variants) of typed π-calculus. Then, we show how to derive in the session π-calculus basic properties, like type safety or complex ones, like progress, by encoding.