PhD Studentship in Science Of Sensor Systems Software (S4)
Department Of Computer Science
University Of Liverpool

Description

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 2018, 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 commonality and abstractions across these systems, for example in terms of sensor geography, shape, neighbours, movement, protocol, reliability, etc.

Potential Supervisors

For informal enquires please contact Clare Dixon (cldixon [at] liverpool.ac.uk).

Applications and Scholarship

This is a fully funded PhD Scholarship, available to both UK and EU students, and covers both tuition fee and living expenses for three years in duration. This PhD studentship is still available. Please contact the above team for more information. Please mention "S4'' and the potential project(s) you would be interested in on your application.

Potential Projects

A variety of potential projects are available within the above general description. Some suggestions are below.

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.

Sample 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.

Proposed Supervisors: Fisher, Linker, Dixon

Fault Tolerance for Sensor Networks

The use of sensors for monitoring for example chemical spills, earth movements near rail or road, pollution in rivers etc is increasingly viable. Together groups of sensors can provide data that can be used to provide early warning of problems. However results might be affected by the distribution and location of individual sensors, sensor calibration issues, degradation and failure. This project involves developing and applying formal verification techniques to model networks of sensors and analyse different types of failure to ensure the robustness of sensor networks.

Sample publication: Gainer, Linker, Dixon, Hustadt and Fisher. Investigating Parametric Influence on Discrete Synchronisation Protocols using Quantitative Model Checking, 14th International Conference on Quantitative Evaluation of Systems (QEST), 2017

Specific expertise/interests: verification; formal methods.

Proposed Supervisors: Dixon, Webster

Languages and Frameworks for Verification of Wireless Sensor-Actuator Networks and the Internet of Things

Wireless sensor/actuator networks are increasingly used in safety- and mission-critical systems. Therefore, verification is essential. However, formal verification is often not used during development of network protocols, as formal models can be difficult to develop by hand. This project involves developing languages and frameworks for protocol design, which would enable formal models to be built automatically as part of the protocol and network design process. This will in turn enable the use of formal verification to improve the reliability of network protocols.

Sample Publications: WASP: A Programming Language for Wireless Sensor Networks.

Archetype-Based Design: Sensor Network Programming for Application Experts, Not Just Programming Experts. Lan S. Bai, Robert P. Dick, Peter A. Dinda.

Sharma et al. Towards Verifying Correctness of Wireless Sensor Network Applications Using Insense and Spin.

Specific expertise/interests: verification, formal methods.

Proposed Supervisors: Webster, Dixon

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?

Sample 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.

Proposed Supervisors: Fisher, Webster

Verification for Large Populations

Sensors or robot swarms may have simple underlying algorithms/programs that interact with each other to provide emergent behaviour. As well as simulations and real robot/sensor experiments, formal verification allows robot swarm or sensor engineers to check the required properties of the network do hold prior to deployment. One issue is that for large networks or populations formal verification may not be viable. This project involves developing and applying formal verification techniques so they can be applied to large networks of individual robots or sensors.

Sample publications: Gainer, Linker, Dixon, Hustadt and Fisher. Investigating Parametric Influence on Discrete Synchronisation Protocols using Quantitative Model Checking. 14th International Conference on Quantitative Evaluation of Systems (QEST), 2017

Konur, Dixon and Fisher. Analysing Robot Swarm Behaviour via Probabilistic Model Checking. Robotics and Autonomous Systems, 60(2):199-213 Elsevier, 2012