Behavioural equivalences for web services
Citation:
Giovanni Bernardi, 'Behavioural equivalences for web services', [thesis], Trinity College (Dublin, Ireland). School of Computer Science & Statistics, 2013, pp 245Download Item:
Bernardi, Giovanni_TCD-SCSS-PHD-2013-05.pdf (PDF) 2.035Mb
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.
Author: Bernardi, Giovanni
Advisor:
Hennessy, MatthewQualification name:
Doctor of Philosophy (Ph.D.)Publisher:
Trinity College (Dublin, Ireland). School of Computer Science & StatisticsNote:
TARA (Trinity's Access to Research Archive) has a robust takedown policy. Please contact us if you have any concerns: rssadmin@tcd.ieType of material:
thesisCollections:
Availability:
Full text availableLicences: