Don't miss our weekly PhD newsletter | Sign up now Don't miss our weekly PhD newsletter | Sign up now

  MOCHA - model checking with agility

   School of Computing

This project is no longer listed on and may not be available.

Click here to search for PhD studentship opportunities
  Dr David Williams , Dr Ben Aziz  Applications accepted all year round  Self-Funded PhD Students Only

About the Project

Applications are invited for a self-funded, 3 year full-time or 6 year part-time PhD project.

The PhD will be based in the School of Computing and will be supervised by Dr David Williams and Dr Ben Aziz.

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. 

Project description

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.

General admissions criteria

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.

Specific candidate requirements

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 ([Email Address Removed]) 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.

Please quote project code COMP5830521 when applying.

Computer Science (8)

Funding Notes

Self-funded PhD students only.
Please for tuition fee information and discounts.