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 .