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:
- Clare Dixon;
- Michael Fisher;
- Sven Linker;
- Matt Webster.
Michael Fisher [Department of Computer Science, University of Liverpool]