Property Preserving Refinements in Formal Software Engineering
PhDs and postgraduate research
Self-funded PhD students only
School of Computing
Applications accepted all year round
Candidates applying for this project may be eligible to compete for one of a small number of bursaries available; these cover tuition fees at the UK/EU rate for three years and a stipend in line with the UKRI rate (£15,009 for 2019/2020). Bursary recipients will also receive a £1,500 p.a. for project costs/consumables.
The work on this project could involve:
- Establishing new theoretical results that prove specific classes of properties are preserved under certain notions of refinement.
- Proposing a novel approach to software engineering that combines refinement checking and model checking to enable properties to be proven of models that could not otherwise be proven via model checking alone.
- Creating new models verifying real world software and systems that demonstrate the added value afforded by combining model checking and refinement
Formal Methods of software and systems engineering apply mathematical rigour to the design and development of high assurance safety and security critical software. They are typically used in domains where programming errors could realistically lead to catastrophic failure or even endanger human life (e.g., defence, aerospace, transport). Refinement is a mechanism used within formal methods to verifiably transform an abstract (high-level) specification of the desired system behaviour into a concrete (low-level) software or system implementation. When this process is conducted iteratively over a number of stages we call this process stepwise refinement. This project shall investigate the preservation of properties (checkable via model checking) through such a series of stepwise refinements. In particular, we shall investigate which classes of liveness properties (which require that some desired behaviour must eventually occur) are preserved under various notions of refinement. The approach developed will enable properties to be proven of models that could not otherwise be proven via model checking alone. The results shall be applied to meaningful real world case studies to demonstrate the value of combining model checking of properties with refinement based software and systems development.
The outcomes of this three year project will be new theoretical results that show specific classes of properties are preserved under certain notions of refinement alongside new models of real systems that demonstrate the added value afforded by combining model checking and refinement.
Fees and funding
Funding availability: Self-funded PhD students only.
PhD full-time and part-time courses are eligible for the UK Government Doctoral Loan (UK and EU students only).
You'll need a good first degree from an internationally recognised university or a Master’s degree in an appropriate subject. In exceptional cases, we may consider equivalent professional experience and/or qualifications. English language proficiency at a minimum of IELTS band 6.5 with no component score below 6.0.
- Interest in the following: theoretical computer science, software engineering, formal methods, verification and validation, safety and security properties.
- Demonstrable analytical and logical reasoning skills and knowledge of foundations of computer science.
- Ability to think independently, including the formulation of research problems.
- Strong verbal and written communication skills, both in plain English and scientific language for publication in relevant journals and presentation at conferences.
How to apply
We’d encourage you to contact Dr David Williams (email@example.com) to discuss your interest before you apply, quoting the project code.
When you are ready to apply, you can use our online application form. Make sure you submit a personal statement, proof of your degrees and grades, details of two referees, proof of your English language proficiency and an up-to-date CV. Our ‘How to Apply’ page offers further guidance on the PhD application process.
If you want to be considered for this PhD opportunity you must quote project code COMP5320220 when applying.