Supervisor

Suitable for

Abstract

This project lies in the intersetion of model-checking, verification, timed systems, and session types, It aims to tackle the critical challenge of ensuring deadlock-freedom in distributed systems employing timed session types [1, 2] and the application of timed model-checking tools. Timed session types provide a formalism for specifying communication protocols with temporal constraints, while deadlocks pose a persistent threat to system stability. Drawing on established time model-checking tools [3], our objective is to systematically analyse the specified models to detect and scrutinise potential deadlocks. The project also endeavours to build Timed Session Types using a bottom-up approach, and then verify the type-level properties by using a model checker, as in [4]. This research aspires to augment the reliability and correctness of concurrent and distributed systems, contributing to the progression of formal verification techniques.

[1] http://mrg.doc.ic.ac.uk/publications/timed-multiparty-session-types/CONCUR14.pdf

[2] https://mrg.cs.ox.ac.uk/publications/meeting-deadlines-together/

[3] https://uppaal.org/features/ (UPPAAL model checker)

[4] https://dl.acm.org/doi/10.1145/3290343

Using a model-checker to verify the type-level properties for timed binary sessions, along with a literature survey on timed systems with extensions into deadlock-freedom checking could be a mini-project of shorter duration.

Pre-requisites: A student who wishes to learn model checking is welcome. Familiarity with the basic automata theory. Familiarity with the model checking tools will be helpful but not required.