MOCHA - model checking with agility
PhDs and postgraduate research
Funded PhD Project (UK and EU students only)
School of Computing
4 May 21
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 rate for three years and a stipend in line with the UKRI rate (£15,609 for 2021/22). Bursary recipients will also receive a £1,500 p.a. for project costs/consumables.
The work on this project could involve
- Creating models of software systems (using the B-Method and/or Event-B)
- Analysing the models created using linear temporal logic (LTL) model checking
- Making it easier to (re)construct models and (re)check requirements as the needs of users adapt and evolve
- Making the models accessible to a wider audience by creating visually engaging interactive simulations.
All too often, £billions invested in information systems are written off due to project failure; seven in eight IT projects fail to be delivered on time, within budget and satisfying requirements. We need a new way of developing software and information systems that make them more resilient, secure and adaptable to change while reducing time to market.
The MOCHA PhD project aims to improve software/systems development by combining two software engineering approaches that otherwise appear to conflict: agile methods and model checking. Agile methods are used in industry to speed up delivery of working software while also being able to adapt to changing user needs, whereas model checking applies mathematical rigour in the modelling and analysis of high assurance safety and security critical systems.
You will be supported in investigating how to embed B-Method and/or Event-B model checking within the agile Behaviour-Driven Development (BDD) approach to software development. Together, we will contribute new theoretical results for using linear temporal logic (LTL) in B/Event-B refinement, to ensure that properties continue to hold as models are iteratively developed and refined, helping to minimise the effort of (re)checking requirements. We will also make the formal models accessible to a broader set of stakeholders, through the creation of simulations and visualisations with which they can directly engage and interact.
One case study in which we have successfully applied model checking within agile software development has been the development of an automated Gift Aid processing platform, helping UK charities to untap half a £billion of Gift Aid that otherwise goes unclaimed each year. MOCHA shall build upon this success by further embedding model checking with agile software development, making the models accessible to a wider audience through interactive visualisations, and making it easier to recheck models as requirements and/or system designs evolve.
You'll need a good first degree from an internationally recognised university (minimum upper second class or equivalent, depending on your chosen course) 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
Prior knowledge/experience in either agile software development or formal methods, with the expectation to develop knowledge and expertise in both during the PhD.
How to apply
We’d encourage you to contact Dr David Williams (firstname.lastname@example.org) 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 funded PhD opportunity you must quote project code COMP5830521 when applying.