[robotics-worldwide] [jobs] Funded PhD - Verification Techniques for Swarm Robotics
RoboChart is a domain-specific notation for modelling mobile and autonomous
robot controllers, their hardware, and their environments. RoboChart models
can be checked by automated analysis, including techniques for simulation,
testing, model checking, and theorem proving. These techniques overlap
substantially, and each has its pros and cons. This project specifically
concerns model checking and theorem proving.
Model checking is a push-button technique, but this is complicated when the
state space is too large; theorem proving handles infinite state spaces,
but usually requires skilled interaction to find proofs. This suggests
combining the two techniques, where theorem proving is used to reduce a
verification problem to finite-state form, so that model checking can then
take over and finish the job. This decomposition of the verification task
forms the basis of SRI’s Symbolic Analysis Laboratory (SAL), a framework
for combining different analysis tools for transition systems via a common
A qualitative property of a program is typically one of the following: a
condition that must be true before execution of the program; a condition
that is guaranteed to be true after its execution; or an invariant that is
guaranteed to hold at all points during its execution. It is qualitative
because it is simply either true or false. A quantitative property, on the
other hand, is typically a qualitative property that holds with probability
As well as qualitative properties, RoboChart supports modelling
quantitative properties involving probabilistic and real-time behaviour.
There is a useful connection between theorem proving and probabilistic
model checking (McIver, 2006, listed below), and we propose to further
develop this result.
Model checking is particularly challenging in the area of swarm robotics.
This is an approach to the coordination of large numbers of simple
individual robots. Collective behaviours emerge from the interactions
between a robot and its peers, and with the environment. Swarm robotics is
inspired by biological metaphors arising from the study of birds, insects,
and other natural organisms where swarming behaviour occurs. Models for
swarm robotics applications have a very large number of states.
This project will explore how verification can be effective in combining
theorem proving and model exploration. The research objective is to
establish that this can be used to check the quantitative performance of
design decisions early in the development cycle. Part of the project is to
learn about the following techniques: theorem proving in Isabelle/HOL;
probabilistic model checking in PRISM and Storm; and statistical model
checking (discrete-event simulation) in PRISM.
If successful, you will be supported for three years. Funding includes:
£14,777 (2018/19 rate) per year stipend,
Home/EU tuition fees,
RTSG (training/consumables/travel) provision.
1. Apply to study
You must apply online for a full-time PhD in Computer Science.
You must quote the project title (Verification Techniques for Swarm
Robotics Studentship) in your application.
There is no need to write a full formal research proposal as this
studentship is for a specific project.
2. Provide a personal statement of 500-1,000 words with your initial
thoughts on the research topic.
Selected relevant publications on verification are as follows:
3. Leonardo de Moura, et al. SAL 2. Proceedings CAV 2014. Springer Lecture
Notes in Computer Science vol. 3114 pp.496-500 2004
4. Annabelle McIver. Quantitative Refinement and Model Checking for the
Analysis of Probabilistic Systems. Proceedings FM 2006. Springer Lecture
Notes in Computer Science vol. 4085 pp.131-146 2006
5. Simon Foster, Frank Zeyda, and Jim Woodcock. Isabelle/UTP: A Mechanised
Theory Engineering Framework. 5th International Symposium on UTP. Springer
Lecture Notes in Computer Science vol. 8963 pp.21-41 2015