Science Of Sensor Systems Software - Languages and Frameworks for Verification of Wireless Sensor-Actuator Networks and the Internet of Things

A PhD position is offered in the Department of Computer Science starting in October 2018, and associated with the Science of Sensor Systems Software (http://www.dcs.gla.ac.uk/research/S4/) 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. For more details see http://cgi.csc.liv.ac.uk/~clare/projects/S4PhDStudentship.html

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. The project is flexible within this general area given the applicant’s background and interests and a sample project is given below.

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.