Funded PhD Studentship

Do you have, or are you about to achieve, either a first class degree or a distinction at masters level in Computer Science or Mathematical Logic, and are you seriously interested in studying for a PhD?

The Department of Computer Science offers a PhD position, starting in October 2017, and associated with the Science of Sensor Systems Software research programme.

This position is available to both UK and EU students, and we are looking for outstanding candidates able to undertake PhD study on formal verification for wireless sensor networks.

This could cover a broad range of systems/protocols, such as synchronization protocols, gossip protocols, ad-hoc networks, etc, and a wide variety of potential formal verification techniques, such as theorem-provers, model-checkers, SMT solvers, runtime verification, etc. Generally, we wish to study, formalise and utilise commonaility and abstractions across these systems, for example in terms of sensor geography, shape, neighbours, movement, protocol, reliability, etc.

Relevant Publications:

Konur, Dixon, and Fisher. Analysing Robot Swarm Behaviour via Probabilistic Model Checking. Robotics & Autonomous Systems 60(2):199-213, 2012.
Dixon, Fisher, Winfield, and Zeng. Towards Temporal Verification of Swarm Robotic Systems. Robotics & Autonomous Systems 60(11):1429-1441, 2012.
Fisher, Dennis, and Webster. Verifying Autonomous Systems. Communications of the ACM 56(9):84-93, 2013.
Konur and Fisher. A Roadmap to Pervasive Systems Verification. Knowledge Engineering Review 30(3):324-341, 2015.

To give candidates an idea of the variety of projects available within the above general description, sample detailed project instantiations are provided below. (Note that this is not an exhaustive list)

How to Apply:

Instructions on how to apply, and the online form to use, can be found at

https://www.liverpool.ac.uk/computer-science/postgraduate/phdstudy/applications

Deadline for applications is 17th April 2017.

Example: Reliable Reconfiguration of Sensor Networks

One or more distinguished agents within the network have self-awareness and fault tolerance responsibilities. The agent knows the current `goal' of network and can monitor the network's behaviour and detect when the network is not functioning appropriately. As well as the network activity, the agent controls the network architecture (i.e. interconnections and internal node programming). When something concerning the world/software/hardware/goal changes, the agent must ensure that the network remains effective. How can it achieve this? And how can we formally verify this?

Relevant Publication: Dennis, Fisher, Aitken, Veres, Gao, Shaukat, and Burroughes. Reconfigurable Autonomy. Künstliche Intelligenz 28(3):199-207, 2014.

Specific expertise/interests: agents; autonomy; software architectures; formal methods.

Example: Combining Model-Checkers

Model checking is a well-established technique for the formal verification of concurrent, distributed, and agent-based systems. In recent years, the need for more complex logical frameworks, for example combining probabilistic and real-time aspects, as well as knowledge, belief, goals, etc., in order to verify realistic systems has appeared. Rather than generating a bespoke formal verification system for each new combination, we here look at both the theoretical and practical issues concerned with taking a modular approach to combinations of logics. We explore how to utilize existing model-checkers for component logics in a modular way to construct a verification system for the required combinations.

Relevant Publication: Konur, Fisher, and Schewe. Combined Model Checking for Temporal, Probabilistic, and Real-time Logics. Theoretical Computer Science 503:61-88. Elsevier, 2013.

Specific expertise/interests: model-checking; complexity or implementation; formal methods.

Example: Synchronisation Protocol Verification

Network wide communication protocols are often used to synchronise information or processes across the whole network. These must be scaleable, flexible, resilient, and efficient. How do we verify these? How do we abstract from implementation details? What formal verification tools are most appropriate?

Relevant Publication: Gainer, Dixon, and Fisher. Routes Towards Formal Verification of Network Synchronisation using Nature-Inspired Pulse-Coupled Oscillators, 2014.

Specific expertise/interests: model-checking; proof; abstractions; modelling.

Potential PhD Supervisors:

Michael Fisher [Department of Computer Science, University of Liverpool]