An Institution for TLA+: A Framework for Interoperability

About the Project

There are a plethora of formal methods used for the specification and verification of critical systems. Each of these is suitable for modelling and anlaysing various aspects of system operation. For example, temporal logics (such as in TLA+) allow us to examine a system’s evolution over time, while first-order state-based methods (such as Event-B) can provide proofs of correctness including safety invariant preservation using a set theoretic modelling notation. Temporal logic specifications are typically verified using model-checking which exhaustively examines the state base. While first-order logic based formalisms tend to rely on theorem proving approaches. Both analysis methods have benefits and drawbacks. Model-checking is automatic and fast to find bugs but struggles with large state spaces. Theorem proving often requires proof interaction from the user but can provide a complete guarantee for all values in the state space without timing out. Combining these disparate approaches into a holistic and mathematical framework is clearly desirable.

The theory of institutions provides a category theoretic framework that allows us to define formal semantics, robust modularization constructs and logical interoperability between formal methods. The formalisms that are used in formal specification and verification can thus be represented as institutions to give access to these benefits. In this project, we focus on the combination of the TLA+ and Event-B formal methods. Both of these are chosen not just because they are theoretically interesting but they are industrial-strength formal methods. This will ensure that our results contribute to a formal, logical and practical grounding for model driven development.

The specific deliverables for this project are:

1. Define an institution for the flavor of temporal logic used by the TLA+ framework. This will include developing a tool to translate raw TLA+ specifications into the language of the institution as well as a mechanized proof of institutional correctness using our pre-existing framework in the Coq theorem prover.
2. Examine modularisation in the context of the TLA+ institution. To do this, we must prove that our institution for TLA+ is well-behaved by admitting pushouts and preserving the institution theoretic amalgamation property.
3. Define institution (co)morphisms between the TLA+ institution and the pre-existing institution for Event-B.
4. Tool support for these developments by extending the Heterogeneous Toolset (Hets).
5. A suite of case studies drawn from various critical domains to explicate the approach.

The ideal candidate for this PhD project will possess a strong background in formal reasoning, logics and mathematics.

Eligibility

Applicants should have, or expect to achieve, at least a 2.1 honours degree or a master’s (or international equivalent) in a relevant science or engineering related discipline.

Funding

Excellent candidates will be nominated for competence-based funding. The funding covers tuition fees and provides a tax-free stipend based on the UKRI rate (£20,780 for 2025/26). We expect the stipend to increase each year. This 3.5 year PhD project is due to start in October 2026 to January 2027.

Self-funded students are welcome to apply.

We recommend that you apply early as the advert may be removed before the deadline.

Before you apply

We strongly recommend that you contact the supervisor for this project before you apply. Please include details of your current level of study, academic background and any relevant experience and include a paragraph about your motivation to study this PhD project.

How to apply

Apply online through our website: https://uom.link/pgr-apply-2425

When applying, you’ll need to specify the full name of this project, the name of your supervisor, if you already having funding or if you wish to be considered for available funding through the university, details of your previous study, and names and contact details of two referees.

Your application will not be processed without all of the required documents submitted at the time of application, and we cannot accept responsibility for late or missed deadlines. Incomplete applications will not be considered.

After you have applied you will be asked to upload the following supporting documents:

• Final Transcript and certificates of all awarded university level qualifications
• Interim Transcript of any university level qualifications in progress
• CV
• Supporting statement: A one or two page statement outlining your motivation to pursue postgraduate research and why you want to undertake postgraduate research at Manchester, any relevant research or work experience, the key findings of your previous research experience, and techniques and skills you’ve developed. (This is mandatory for all applicants and the application will be put on hold without it).
• Contact details for two referees (please make sure that the contact email you provide is an official university/work email address as we may need to verify the reference)
• English Language certificate (if applicable)

If you have any questions about making an application, please contact our admissions team by emailing FSE.doctoralacademy.admissions@manchester.ac.uk.