Simulation & Verification

As the design for a piece of software, hardware, or model becomes more elaborate, it becomes difficult to ensure that it's really working how you think it's working.  Process algebras (or process calculi) are tools from computer science that allow you to prove whether a certain process can ever exhibit a behaviour.  This is particularly useful for reasoning about systems in where processes can happen in parallel, which makes them well-suited for studying biological systems: many processes occur simultaneously within a cell, and these processes can have an important impact on one another.


While process algebras have been used to model biological systems before, they have failed to grain traction within the systems biology community as a mainstream method.  This stems largely from their roots in theoretical computer science, resulting in publications and methods that often require a great deal of specialist knowledge to understand.  We wanted to make a new process algebra that was accessible to nonspecialists so that the power of the method could be packaged in something that was also easy to use.  The end result was the Beacon Calculus.  Models written in the Beacon Calculus are concise, easy to encode, and straightforward to communicate to experimentalists.  It is also straightforward to modify and extend models written in the Beacon Calculus so that users can freely experiment with different hypotheses about how a mechanism might work by only changing a term or two.


The above snippet shows source code for a model of DNA replication: firing factors (FF) cause replication origins (ORI) to fire, at which time they start a leftward-moving replication fork (FL) and a rightward-moving replication fork (FR) that replicates the chromosome.  The model is expressed in only a few lines of code and thousands of simulations can be run in seconds.  When we simulate the model using our Beacon Calculus Simulator (bcs) software, we obtain a good fit to replication timing data for S. cerevisiae chromosome II:


Here, however, we have just shown one chromosome.  The model above actually encodes replication for all 16 chromosomes in the S. cerevisiae genome which can be simulated in seconds using bcs:


In addition to being scalable, we also designed the Beacon Calculus such that models would be easy to modify.  If we want to study genome-wide replication fork stalling, then we only have to make the changes to the above model shown in red:


This example has focused on DNA replication, but the Beacon Calculus can be used across diverse areas of biological research.  Thus far, the topics that the Beacon Calculus has been used to study include:

  • DNA replication,

  • multisite phosphorylation and ultrasensitive receptors,

  • transcription (including replication-transcription interactions),

  • DNA damage response,

  • growth of centrioles.

If you're interested in using the Beacon Calculus for your application, we would be happy to hear from you.

Corresponding publications:

Boemo, M.A.†, Cardelli, L., Nieduszynski, C.A. (2020) The Beacon Calculus: A formal method for the flexible and concise modelling of biological systems. PLoS Computational Biology 16:e1007651. [bioRxiv[DOI:​10.1371/journal.pcbi.1007651]

Corresponding software: 

bcs is available on GitHub and we maintain a manual with examples.