Correctly communicating software: Distributed, asynchronous, and beyond

We rely on software in every aspect of our everyday lives, so it is crucial that this software functions reliably. The majority of software consists of smaller pieces of software that cooperate by communicating. Reliable communication is therefore imperative to the reliability of software. Ideally, software is guaranteed to function correctly by construction; this contrasts common practice, where software is (non-exhaustively) tested for potential problems, or problems are even encountered only when it is in use.

This dissertation develops techniques that ensure that software communicates correctly by construction. The main component herein is communication protocols that describe precisely what is expected of the communication of pieces of software. These protocols are then used to guide the development of correctly communicating software.

The approach is mathematical, taking heavy inspiration from logical reasoning. Logic provides precise techniques to reason about the communication resources of software, that make guaranteeing correctness straightforward. However, this straightforwardness comes with limitations: the techniques are restricted in the communication patterns they support. An example restriction is that when more than two pieces of software need to communicate, they can only do so through a single point of connection. In practice, pieces of software can communicate with each other directly, without such limitations.

Hence, the theme of this dissertation is pushing the boundaries of logic reasoning for communicating software. The goal is getting closer to reliable communication by construction for realistic software. As such, the thesis develops new and improves existing techniques based on logic, while maintaining correctness guarantees.