So you want to do a PhD?
I'm part of a group working on process algebra and verification.
For information on my interests, see my
Research page.
My main interest currently is the use of formal methods, particularly
probabilistic languages to describe biological systems. There are two main
strands:
- Epidemiology (in collaboration with
Dr Rachel Norman of
Mathematics). The idea is to use a process algebra approach to
describing disease systems, and to develop analytical techniques to
allow the dynamics of the system to be explored. An important facet of
the work compares the process algebra approach with a more traditional,
differential equation based, approach. Currently
Chris McCaig is working on
this, using WSCCS and automatically generating mean field equations from
that. Further ways to develop this include using
PEPA to explore continuous behaviour.
- Description of biochemical networks. I have declarative
description of the RKIP pathway, but an interesting approach should be
to model the system in more detail using the method above and treating
individual receptors as agents.
I'm also interested in the the semantics of LOTOS (a formal
description technique) and the development of a framework for reasoning
about LOTOS specifications, which is more compact than the standard
framework. Until recently this work was funded under the
DIET project.
Briefly, we've utilised a symbolic framework developed by Hennessy and
Lin to encode the formal description technique LOTOS (which has process
algebra plus data). This means that we now have a finite representation
for LOTOS semantics (making LOTOS behaviours amenable to
automated reasoning).
Anything related to that would be suitable as a PhD project with me.
Possible projects include:
-
Although LOTOS is used, its uptake has been hampered by the lack of
powerful tools for validation and verification.
Having the symbolic framework should allow us to address
that problem more effectively. Current developments include a
bisimulation algorithm and model checkers. These are prototypes, so
there's lots of room for making these tools more sophisticated and
acceptable to software engineers.
-
Other notations, such as UML, are more popular in industry than
formalisms such as LOTOS. Can we provide a framework in which software
engineers can use notations they're familiar with, but which allow us to
carry out rigorous analysis behind the scenes by relating them to, e.g.
LOTOS and the modal mu-calculus.
-
Testing theory for LOTOS is quite well developed, with work on
conformance relations and so on. A similar theory could be developed
based on symbolic semantics. This work would be in conjunction with Prof
Turner, with applications to medical radiotherapy equipment.
-
Enriching the formalism and encoding that extension in the symbolic
framework, e.g. consider some operators from ELOTOS (an
enhanced version of LOTOS) such as time, or imperative features, or
maybe probabilistic aspects.
Having said all that, I'm open to suggestions, so why not
email me .