[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
Dear all,
We have a fully funded PhD scholarship available in the School of Computer
Science at the University of St Andrews on ‘Refactoring Fault-Tolerant
Communication Protocols’.
Any potential candidates are advised to contact Adam Barwell
([email protected]) for more information. Formal applications can be made
through the School’s postgraduate research portal [1].
A description of the project can be found below and full details of the project
can be found here:
https://urldefense.com/v3/__https://www.findaphd.com/phds/project/refactoring-fault-tolerant-communication-protocols/?p165748__;!!IBzWLUs!Vmjnp7wt0f_QN37wtPKm3z2zlPfU99UK_N5vO_8KAND5DFYHTsqT4fyYifuNrkYM1w-imOp0D5TxdB-IfDE53oi8RzbwbJQYKP4$
The positions are open for both UK and international applications.
Kind regards,
Adam
[1]
https://urldefense.com/v3/__https://www.st-andrews.ac.uk/computer-science/prospective/pgr/how-to-apply/__;!!IBzWLUs!Vmjnp7wt0f_QN37wtPKm3z2zlPfU99UK_N5vO_8KAND5DFYHTsqT4fyYifuNrkYM1w-imOp0D5TxdB-IfDE53oi8RzbwRSHDJuU$
----
Project Title: Refactoring Fault-Tolerant Communication Protocol
Concurrent and distributed systems are now standard. Yet programming approaches
have failed to keep pace. These systems are prone to a range of subtle and
difficult-to-debug errors, e.g. communication mismatches, deadlocks, and
livelocks. Session Types aim to address these issues via high-level formal
specifications of communications protocols. An advantage of this approach is
that session types enable static guarantees of desirable behavioural
properties, e.g. deadlock-freedom and liveness.
Recent work has focussed on extending session types to support fault-tolerance,
enabling protocols with real-world crash-handling behaviours, e.g. failover and
the circuit-breaker pattern. Furthermore such approaches enable a gradual
approach to introducing failure-handling, whereby a fully reliable protocol can
be made fault-tolerant one participant at a time. Nevertheless, a
fault-tolerant protocol can be significantly larger and more complex than the
fully-reliable protocol from which it is derived. Moreover, ensuring that the
desired transformations are effected uniformly and correctly both from a
protocol and implementation perspectives can be a laborious and error-prone
process.
This PhD project will address this issue by leveraging semi-automatic program
transformation techniques from refactoring to develop automatic methods to
introduce and manipulate fault-tolerant behaviours in communications protocols.
The project will explore the theoretical underpinnings of such transformations,
ensuring that the guarantees provided by session types are preserved.
Additionally, the project aims to develop tooling to enable application of the
developed techniques to real-world code.
