FindAPhD Weekly PhD Newsletter | JOIN NOW FindAPhD Weekly PhD Newsletter | JOIN NOW

Formally based Mutation Testing of Distributed and Concurrent Applications

   Centre for Digital Innovation

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

Click here to search for PhD studentship opportunities
  Dr Qiang Guo, Prof V Chang, Dr Chunyan Mu  No more applications being accepted  Funded PhD Project (Students Worldwide)

About the Project

Testing is an important yet expensive part of the process of software development. It usually accounts for 50% of the total cost. Manually testing a system is costly and error prone. Approaches that automate or semi-automate sections of software testing may significantly improve the efficiency and quality of the software development process. With nowadays the architectures of software applications tending to be distributed and concurrent, innovative techniques and formally based supportive tools for testing distributed and concurrent applications become highly demanded.

Mutation testing is a software testing technique that is based on artificially seeding the implementation with small faults (called mutating) by applying mutation operators and determining whether testing identifies these faults. A mutated program is called a mutant and if a test set distinguishes the mutant from the original implementation, the mutant is killed, otherwise the mutant is alive. The advantage of the mutation testing lies in that each mutant reflects a type of fault in the implementation and, if a derived test fails to kill a mutant, it potentially unveils an undiscovered bug. Mutation testing has a wide application in testing industrial programs. One of the successful examples can be found in Facebook London where a research group applies mutation-based techniques along with search-based optimisation techniques to test Facebook's products.

However, there are few examples of mutation testing applied to distributed and concurrent applications. This may be due to the nondeterministic characteristics of almost all distributed and concurrent applications. In the meantime, formal methods such as Finite State Machines (FSMs) and model-checking based techniques prove effective in validating and verifying nondeterministic characteristics [3 – 7]. This motivates us to work on a new framework to test distributed and concurrent systems by combining the uses of formal methods and mutation testing techniques. Moreover, to automate the testing process, in the proposed project, we will be dedicated to developing a formally based mutation testing tool which, we believe, can help to strengthen the collaborative links with some potential industrial partners.

Methodologies and objectives

The project is initiated and inspired from our previous EPSRC research work FORSE [1] and EU FP7 ProTest [2] and the recent work on testing a fast payment platform. The applied methodologies and the proposed objectives can be summarised as follows:

  1. Prototype a set of effective mutation operators that can be used to alter program source codes with an objective to discover hard-to-find bugs. Mutation operations should be proceeded at system's semantic level
  2. Define a set of rules to work on higher order mutation test with an objective to discover fault coupling effects. A fault coupling effect defines two faults occur in order with the observation of the first being masked by the second.
  3. Apply formal methods such as model-checking based techniques to verifying property-based mutation behaviour.
  4. Using Meta-heuristic Optimisation Technologies (MOTs) such as Genetic Algorithms (GAs), Simulated Annealing (SA) and Ant Colony Optimisation (ACO) to optimise the process upon exploring effective mutants.

Expected deliveries

  1. Prototype a framework to generate effective mutants from the distributed and concurrent system under test.
  2. Prototype an effective validation model using formal methods.
  3. Automate the mutation testing process by developing a tool.
  4. Publish research papers.

Research strength and contributions to the school

The proposed project involves research work with an objective to deliver a formally based testing tool. As testing is an essential part in the system development, the proposed project might seek for further KTP collaborations with industrial partners.

The work contributes to university's research profile in the following aspects:

  1. In line with the school's research and innovative strategies upon boosting industrial productivities, the project works on prototyping an innovative framework to test distributed and concurrent systems, and then integrating such a framework to an industrial oriented testing tool. The success of such a tool helps to strengthen the links between our research groups and some industrial partners, which might potentially bring in KTP research funding.
  2. The work contributes to enhancing school's research profile by bringing in a new research area - formally based testing of distributed and concurrent systems. The work will be carried out under a multicore environment. To optimise test generations, pattern based parallel programming techniques will be applied with an objective to maximise the use of available computational resources.


Nowadays, the architectures of software applications tend to be distributed and concurrent. Finding ways to effectively test distributed and concurrent applications become highly demanded. Mutation testing has demonstrated its effectiveness in testing sequential programs while formal methods prove effective in verifying distributed and concurrent architectures. In this PhD project, we will supervise students to combine the uses of these two techniques to prototype a new testing model that can be suitable for testing a distributed and concurrent platform. The derived model will be later integrated to the development of a formally based testing tool to support the industrial testing activities, which, we believe, can potentially help to bring in KTP research funding.

Entry Requirements

Applicants should hold or expect to obtain a good honours degree (2:1 or above) in a relevant discipline. A masters level qualification in a relevant discipline is desirable, but not essential, as well as a demonstrable understanding of the research area. Further details of the expected background may appear in the specific project details. International students will be subject to the standard entry criteria relating to English language ability, ATAS clearance and, when relevant, UK visa requirements and procedures.

How to Apply

Apply online at:

Please use the Online Application (Funded PHD) application form. When asked to specify funding select “other” and enter ‘RDS’ and the title of the PhD project that you are applying for. You should ensure that you clearly indicate that you are applying for a Funded Studentship and the title of the topic or project on the proposal that you will need to upload when applying. If you would like to apply for more than one project, you will need to complete a further application form and specify the relevant title for each application to a topic/project.

Funding Notes

The Fees-Paid PhD studentship will cover all tuition fees for the period of a full-time PhD Registration of up to four years. Successful applicants who are eligible will be able to access the UK Doctoral Loan scheme to support with living costs. The Fully Funded PhD Studentship covers tuition fees for the period of a full-time PhD Registration of up to four years and provide an annual tax-free stipend of £15,000 for three years, subject to satisfactory progress. Applicants who are employed and their employer is interested in funding a PhD, can apply for a Collaborative Studentship.


1) FORSE, Formally based tool support for Erlang development,, 2005.
2) ProTest, Property-based Testing,, 2008.
3) Yue Jia, Mark Harman, “An Analysis and Survey of the Development of Mutation Testing”, IEEE Transactions on Software Engineering, 37(5), pp. 649 - 678, 2010.
4) Qiang Guo, John Derrick, “Formally based tool support for model checking Erlang applications”, International journal on software tools for technology transfer, 13(4), pp. 355-376, 2011.
5) Qiang Guo, “Verifying Erlang/OTP components in muCRL”, International Conference on Formal Techniques for Networked and Distributed Systems, pp. 227-246, 2007.
6) Qiang Guo, John Derrick “Verification of timed Erlang/OTP components using the process algebra muCRL”, ACM SIGPLAN Workshop on Erlang, pp. 55–64, 2007.
7) Qiang Guo, John Derrick, Csaba Hoch, “Verifying Erlang Telecommunication Systems with the Process Algebra muCRL”, International Conference on Formal Techniques for Networked and Distributed Systems, pp. 201-217, 2008
Search Suggestions
Search suggestions

Based on your current searches we recommend the following search filters.

PhD saved successfully
View saved PhDs