Improved Continuous Approximation of PEPA Models through Epidemiological Examples (2009)
Benkirane, Soufiene, Hillston, Jane, McCaig, Chris, Norman, Rachel, Shankland, Carron
We present two individual based models of disease systems using PEPA (Performance Evaluation Process Algebra). The models explore contrasting mechanisms of disease transmission: direct transmission...
Process Algebra Models of Population Dynamics (2008)
McCaig, Chris, Norman, Rachel A., Shankland, Carron
It is well understood that populations cannot grow without bound and that it is competition between individuals for resources which restricts growth. Despite centuries of interest, the question of...
PEPA models of Epidemiology (2008)
Chris Mccaig, Rachel Norman, Carron Shankland
Increasingly, theoretical computer science techniques are being used to tackle biological problems. The question arises: which technique is best suited to the current problem? A related question is:...
Deriving Mean Field Equations from Large Process Algebra Models (2008)
McCaig, Chris, Norman, Rachel A., Shankland, Carron
In many domain areas the behaviour of a system can be described at two levels: the behaviour of individual components, and the behaviour of the system as a whole. Often deriving one from the other is...
C. Shankl, Issn -x, Mathematisch Centrum (smc, The Dutch Foundation, Carron Shankland, ...
and their applications. SMC is sponsored by the Netherlands Organization for Scientific Research (NWO). CWI is a member of
Implementing the modal logic FULL using Ergo [Extended Abstract] (2007)
Peter Robinson, Carron Shankland
Although formal methods are becoming more popular, their uptake is at least partially governed by the success of associated tools. Theorem provers give the most flexibility, but are often difficult...
But What If I Don't Want to Wait Forever? (2007)
We present an abstract model of the leader election protocol used in the IEEE 1394 High Performance Serial Bus standard. The model is expressed in the probabilistic Guarded Command Language. By...
But What If I Don't Want to Wait Forever? (2003)
We present an abstract model of the leader election protocol used in the IEEE 1394 High Performance Serial Bus standard. The model is expressed in the probabilistic Guarded Command Language. By...
A Modal Logic for Full LOTOS based on Symbolic Transition Systems (2002)
Muffy Calder, Savi Maharaj, Carron Shankland
Symbolic transition systems separate data from process behaviour by allowing the data to be uninstantiated. Designing a HML-like modal logic for these transition systems is interesting because of the...
Implementing a modal logic over data and processes using XTL (2001)
Jeremy Bryans, Carron Shankland
Abstract The modal logic FULL is designed to capture strong bisimulation over early symbolic transition systems (STSs) for full LOTOS. It provides a compact way of expressing and verifying properties...
A symbolic semantics and bisimulation for Full LOTOS (2001)
A symbolic semantics for Full LOTOS in terms of symbolic transition systems is dened; the semantics extends the standard one by giving meaning to symbolic, or (data) parameterised processes. Symbolic...
But what if I don't want to wait forever? (Extended Abstract) (2001)
Colin Fidge Software Verification Research Centre Australia Carron Shankland University of Stirling United Kingdom 1
A case study in abstraction using E-LOTOS and the FireWire (2001)
Carron Shankland, Alberto Verdejo
The proposed ISO standard E-LOTOS is used to describe the leader election protocol of the IEEE 1394 serial multimedia bus (iFireWirej). The E-LOTOS language facilitates descriptions at several levels...
A symbolic semantics and bisimulation for Full LOTOS (2001)
Muffy Calder, Carron Shankland
A symbolic semantics for Full LOTOS in terms of symbolic transition systems is defined; the semantics extends the (infinitely branching) standard semantics by giving meaning to data parameterised...
A survey of formal methods applied to leader election (2000)
Savi Maharaj, Carron Shankland
Abstract: We present a survey of formal speci cation techniques applied to the Tree Identify Protocol of the IEEE 1394 High Performance Serial Bus 1. Speci cations written in a variety of formalisms...
An Adequate Logic for Full LOTOS (2000)
Muffy Calder, Savi Maharaj, Carron Shankland
We present a novel result for a logic for symbolic transition systems based on LOTOS processes. The logic is adequate with respect to bisimulation defined on symbolic transition systems. 1...
A Symbolic Semantics and Bisimulation for Full LOTOS (2000)
Muffy Calder, Carron Shankland
A symbolic semantics for Full LOTOS in terms of symbolic transition systems is defined; the semantics extends the (infinitely branching) standard semantics by giving meaning to data parameterised...
Time, E-LOTOS, and the FireWire (1999)
Carron Shankland, Alberto Verdejo
. The proposed ISO standard formal description technique E-LOTOS is used to describe a leader election protocol (that of the IEEE 1394 serial multimedia bus), allowing illustration of the new aspects...
The tree identify protocol of IEEE 1394 (1998)
We specify the tree identify protocol of a high performance serial multimedia bus (IEEE standard 1394 [IEE95]) in three different levels of detail using ¯CRL [GP95]. We propose using the cones and...
Symbolic Bisimulation for Full LOTOS
Carron Shankland, Muffy Thomas, Ed Brinksma
. A symbolic semantics for Full LOTOS in terms of symbolic transition systems is defined, following the approach taken for message passing CCS in [HL95a], altered to take account of the particular...