[Computing Science Logo]


Formal methods can be used to describe and analyse a range of systems. Application of process algebra to biological phenomena is a hot topic in formal methods, bringing all the challenges and rewards of cross-disciplinary work. There is huge potential to make a wider impact with this work, across disciplines. I have several strands in this area, from the epidemiological work I have been engaged in for over ten years, to the more recent work in immunology and collective dynamics of biological systems more generally. My earlier work applied a variety of formal techniques to communications protocols.

I'm the leader of the SICSA Modelling and Abstraction Theme and a member of our local Modelling and Analysis of Complex Systems group.

My interests centre around formal methods and their use in the description and analysis of computer and biological systems. My work can be grouped broadly as follows:

A pervading aspect of my work generally is to undertake larger, more realistic, case studies, in order to demonstrate the utility of various approaches to verification. If you've got any good problems then drop me a line!

Cancer process and therapies

Process algebras can be used to describe a range of biological phenomena. Building on our earlier work on individual-based models of epidemiology, we are modelling the inter- and intra-cellular communications involved in cancer processes and therapies as part of the MEDIC project. Rachel Lintott is the postdoc researcher on this work.

Biological Systems

Process algebras can also be used to describe to biological phenomena. Dr Rachel Norman and I are looking at how to use process algebra to describe disease spread (epidemiology), and exploration of the systems obtained (Eurocast paper). By describing systems using an individual-based method we obtain a different view of the system (traditionally described using population level Ordinary Differential Equations).

Chris McCaig is our research fellow, and Soufiene Benkirane is our PhD student in this area. Chris focussed on an automatic method for generating mean field difference equations from WSCCS, and also an accurate approach to describing disease transmission. The former gives us a rigorous way of relating individual-based models to population-based models, and thereby allows us to investigate questions of epidemiology based on observations of individual behaviour. We had a recent paper in Algebraic Biology on population growth.

Soufiene's work centres around the use of PEPA, another process algebra. The goal is to determine the most useful language constructs for describing epidemiology. We had a paper in FBTC (From Biology to Concurrency) in the summer.

During my sabbatical (Autumn 2004) I visited the Bioinformatics Research Centre at the University of Glasgow. I looked at describing and analysing biochemical networks using a logical, declarative approach. I'd like to apply the techniques we've developed for epidemiology to modelling these networks.

LOTOS and Symbolic Semantics

A core interest has been developing a symbolic framework for reasoning about LOTOS. The symbolic approach gets round the problem of infinite branching in the underlying semantics of LOTOS, and the new semantics is more amenable to automated reasoning. This is joint work, mainly with Muffy Calder of the University of Glasgow, Savi Maharaj and Jeremy Bryans of the University of Stirling.

On top of the new symbolic semantics we've defined a symbolic bisimulation equivalence (in the style of Hennessy and Lin's work for message passing CCS), and a modal logic. The modal logic is basically HML plus data and provides a means of specifying desirable system properties in a more abstract fashion. The symbolic approach separates reasoning about data from reasoning about processes as much as possible (but without losing the information the data gives us). We assume we have access to an oracle which can prove statements about data (although the expressivity of the data language of LOTOS means that such statements may be undecidable).

To find out more about the symbolic work go to the DIET project pages. Although no longer funded, the work is still ongoing. If you'd like to be involved let me know.

I have been interested in verification of properties of LOTOS specifications for a while (15 years). My Ph.D. thesis looks at this area, specifically addressing the problem of proving two LOTOS specifications equivalent (using term rewriting techniques).

To find out more about LOTOS, have a look at Ken Turner's WELL page.


In summer 1997 I was a visiting fellow of the Programming Research Group of the University of Amsterdam. The fellowship was part of the EXPRESS project. While there I worked with several people at the University and also from the Concurrency and Real Time Group at CWI, namely Jan Friso Groote, Alban Ponse, Judi Romijn and David Griffioen. The work carried out was a specification and verification study of the tree identify protocol of the 1394 serial bus. This was presented at the FMICS workshop. Further work has been carried out with Mark van der Zwaag at CWI, and the resulting paper was published in FACS.

The FireWire is a good case study, with many possibilities for different modelling approaches, and some subtle complexities. I've also looked at it through E-LOTOS glasses (with Alberto Verdejo), and using pGCL (see below).

In 2001 I and Savi Maharaj organised a workshop on the FireWire, bringing together several people applying formal methods to the FireWire example. Selected papers from this workshop form the special issue of Formal Aspects of Computing 14(3). Savi and I also wrote a survey of formal approaches to the FireWire (published in JUCS).

Probabilistic descriptions

During my sabbatical (Autumn 2000) I visited Colin Fidge at the SVRC in Queensland. We investigated probabilistic aspects of specification and verification of the FireWire root contention protocol using pGCL (probabilistic Guarded Command Language).

[Books] Publications

See my Publications page for details.

Please email me if you want any more information.

[] Research   [] Teaching   [] Personal   [Home] Home

Dr Carron Shankland    Email: carron at cs.stir.ac.uk [email me]   

Last revision: 14th May 2014