Behavioural equivalences for web services

Abstract

This thesis is a foundational and systematic investigation of the principles which ensure that a piece of communicating software can be replaced by another piece of communicating software, without hindering the operations of the pre-existing system. By “foundational” we mean that our approach is mathematical; we define in formal terms notions such as “system correctness” and “safe software replacement”, thereby providing reasoning techniques (i.e. proof methods) for the notions themselves. By “systematic” we mean that our results lay bare the principles which allow the replacement of software in all the roles it can take: servers, clients and peers. The investigation presented in this thesis stems from practical questions, such as the following: Q1) if the client r is satisfied by the server p1, what relation between p1 and a server p2 guarantees that p2 satisfies r? Q2) if the server p satisfies the client r1, what relation between r1 and a client r2 guarantees that p satisfies r2? Q3) if the peer p1 satisfies and is satisfied by the peer q, what relation between p1 and a peer p2 guarantees that p2 satisfies and is satisfied by q? The questions above are motivated by the practice of software maintenance; as they stand, though, they are rather vague, and a priori it is clear neither what they really mean, nor how to answer them. Our foundational approach allows us to formulate the precise meaning of the questions above, and to answer them. The contributions of this thesis are the following: • we enrich the standard testing theory of [De Nicola and Hennessy, 1984] with new pre-orders, one for clients and one for peers, and present their behavioural characterisations (Theorem 4.2.37, Theorem 4.3.17); • we introduce a compliance relation inspired to [Castagna et al., 2009; Laneve and Padovani, 2007], the pre-orders that arise from it, respectively for servers, clients, and peers; and we present the behavioural characterisations of these pre-orders (Theorem 5.1.15, Theorem 5.2.25, Theorem 5.3.26); • we show a fully abstract model of the sub-typing `a la [Gay and Hole, 2005] on first-order session types (Theorem 6.3.4). We define the model in two alternative ways, one uses to the testing theory, and one uses to the compliance theory (Proposition 6.5.19). The model justifies and explains in behavioural terms the sub-typing relation; • we generalise the first-order model so as to exhibit a fully abstract model of the sub-typing on higher-order (i.e. standard) session types (Theorem 8.4.9). We also explain which conditions are necessary and sufficient to extend the first-order model to the higher-order setting.