Formal Methods for Checking the Consistency of Biological Models

  • Allan ClarkEmail author
  • Vashti Galpin
  • Stephen Gilmore
  • Maria Luisa Guerriero
  • Jane Hillston
Conference paper
Part of the Advances in Experimental Medicine and Biology book series (AEMB, volume 736)


Formal modeling approaches such as process algebras and Petri nets seek to provide insight into biological processes by using both symbolic and numerical methods to reveal the dynamics of the process under study. These formal approaches differ from classical methods of investigating the dynamics of the process through numerical integration of ODEs because they additionally provide alternative representations which are amenable to discrete-state analysis and logical reasoning. Backed by these additional analysis methods, formal modeling approaches have been able to identify errors in published and widely-cited biological models. This paper provides an introduction to these analysis methods, and explains the benefits which they can bring to ensuring the consistency of biological models.


Biological Model Invariant Analysis Label Transition System Process Algebra Species Definition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.



Clark, Guerriero, Gilmore, and Hillston are supported by the Centre for Systems Biology at Edinburgh. The Centre for Systems Biology at Edinburgh is a Centre for Integrative Systems Biology (CISB) funded by BBSRC and EPSRC, reference BB/D019621/1. The authors benefited from an introduction to invariant generation by Peter Kemper during his time as a SICSA Distinguished Visiting Fellow.


  1. 1.
    Clark A, Gilmore S, Hillston J, Kemper P (2010) Verification and testing of biological models. In: Proc winter simulation conference (WSC), December 2010, pp 620–630Google Scholar
  2. 2.
    Calder M, Duguid A, Gilmore S, Hillston J (2006) Stronger computational modelling of signalling pathways using both continuous and discrete-state methods. In: Proc 4th international conference on computational methods in systems biology (CMSB’06) (Lecture notes in computer science), vol 4210, pp 63–77Google Scholar
  3. 3.
    Reisig W (1985) Petri nets: an introduction. Springer-Verlag, New YorkGoogle Scholar
  4. 4.
    Păun G (2002) Membrane computing: an introduction. Springer-Verlag, New YorkCrossRefGoogle Scholar
  5. 5.
    Danos V, Laneve C (2004) Formal molecular biology. Theor Comput Sci 325(1):69–110CrossRefGoogle Scholar
  6. 6.
    Priami C, Regev A, Silverman W, Shapiro E (2001) Application of a stochastic name-passing calculus to representation and simulation of molecular processes. Inf Process Lett 80(1):25–31CrossRefGoogle Scholar
  7. 7.
    Ciocchetta F, Hillston J (2009) Bio-PEPA: a Framework for the Modelling and Analysis of Biological Systems. Theor Comput Sci 410(33–34):3065–3084CrossRefGoogle Scholar
  8. 8.
    Kwiatkowski M, Stark I (2008) The continuous π-calculus: a process algebra for biochemical modelling. In: Proc 6th international conference on computational methods in systems biology (CMSB’08) (Lecture notes in computer science), no 5307. in, Springer-Verlag, Berlin Heidelberg, Germany, pp 103–122Google Scholar
  9. 9.
    Gillespie DT (1977) Exact stochastic simulation of coupled chemical reactions. J Phys Chem 81(25):2340–2361CrossRefGoogle Scholar
  10. 10.
    Duguid A, Gilmore S, Guerriero ML, Hillston J, Loewe L (2009) Design and development of software tools for Bio-PEPA. In: Proc winter simulation conference (WSC’09). IEEE Press, Piscataway, NJ, USA, pp 956–967Google Scholar
  11. 11.
    Python Programming Language Official Website (2011)
  12. 12.
    Rohr C, Marwan W, Heiner M (2010) Snoopy, a unifying Petri net framework to investigate biomolecular networks. Bioinformatics 26(7):974–975PubMedCrossRefGoogle Scholar
  13. 13.
    MathWorks MATLAB (2011)
  14. 14.
    Calzone L, Fages F, Soliman S (2006) BIOCHAM: an environment for modeling biological systems and formalizing experimental knowledge. Bioinformatics 22(14):1805–1807PubMedCrossRefGoogle Scholar
  15. 15.
    Peleg M, Yeh I, Altman R (2002) Modeling biological processes using Workflow and Petri Net models. Bioinformatics 18(6):825–837PubMedCrossRefGoogle Scholar
  16. 16.
    Heiner M, Gilbert D, Donaldson R (2008) Petri Nets for Systems and Synthetic Biology. In: Proc formal methods for computational systems biology (SFM’08) (Lecture notes in computer science), vol 5016. Springer-Verlag, Berlin Heidelberg, Germany, pp 215–264Google Scholar
  17. 17.
    Martinez J, Manual Silva (1982) A simple and fast algorithm to obtain all invariants of a generalized petri net. In: Proc selected papers from the first and the second european workshop on application and theory of petri nets. Springer-Verlag, London, UK, pp 301–310Google Scholar
  18. 18.
    Guerriero ML (2009) Qualitative and quantitative analysis of a Bio-PEPA model of the Gp130/JAK/STAT signalling pathway. Trans Comput Syst Biol XI 5750:90–115CrossRefGoogle Scholar
  19. 19.
    Sen K, Viswanathan M, Agha G (2005) On statistical model checking of stochastic systems. In: Proc computer aided verification (Lecture notes in computer science), vol 3576. Springer-Verlag, Berlin Heidelberg, Germany, pp 266–280Google Scholar
  20. 20.
    Younes HLS, Simmons RG (2006) Statistical probabilistic model checking with a focus on time-bounded properties. Inf Comput 204(9):1368–1409CrossRefGoogle Scholar
  21. 21.
    Ciocchetta F, Gilmore S, Guerriero ML, Hillston J (2009) Integrated simulation and model-checking for the analysis of biochemical systems. In: Proc 3rd international workshop on practical applications of stochastic modelling (PASM’08) (Electronic notes in theoretical computer science), vol 232. Elsevier, Oxford UK, pp 17–38Google Scholar
  22. 22.
    Kemper P, Tepper C (2009) Automated trace analysis of discrete-event system models. IEEE Trans Software Eng 35(2):195–208CrossRefGoogle Scholar
  23. 23.
    Fages F, Rizk A (2007) On the analysis of numerical data time series in temporal logic. In: Proc computational methods in systems biology (CMSB’07) (Lecture notes in computer science), vol 4695. Springer, Berlin, Heidelberg, Germany, pp 48–63Google Scholar
  24. 24.
    Donaldson R, Gilbert D (2008) A model checking approach to the parameter estimation of biochemical pathways. In: Proc computational methods in systems biology (CMSB’08) (Lecture notes in computer science), vol 5307. Springer, Berlin, Heidelberg, Germany, pp 269–287Google Scholar
  25. 25.
    Milner R (1989) Communication and concurrency. Prentice Hall, Hemel Hempstead, UKGoogle Scholar
  26. 26.
    Galpin V, Hillston J (2011) A semantic equivalence for Bio-PEPA based on discretisation of continuous values. Theor Comput Sci 412(21):2142–2161CrossRefGoogle Scholar
  27. 27.
    Galpin V (2011) Equivalences for a biological process algebra. Theor Comput Sci 412(43):6058–6082, DOI 10.1016/j.tcs.2011.07.006CrossRefGoogle Scholar
  28. 28.
    Schoeberl B, Eichler-Jonsson C, Gilles ED, Muller G (2002) Computational modeling of the dynamics of the MAP kinase cascade activated by surface and internalized EGF receptors. Nat Biotechnol 20:270–375CrossRefGoogle Scholar
  29. 29.
    Gong Y, Zhao X (2003) Shc-dependent pathway is redundant but dominant in MAPK cascade activation by EGF receptors: a modeling inference. FEBS Lett 554:467–472PubMedCrossRefGoogle Scholar
  30. 30.
    Box G, Draper N (1987) Empirical model-building and response surfaces. Wiley Series in Probability and Mathematical Statistics, USAGoogle Scholar
  31. 31.
    Knuth DE (1989) The errors of TE X. Software Pract Exper 19:607–685CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media, LLC 2012

Authors and Affiliations

  • Allan Clark
    • 1
    Email author
  • Vashti Galpin
    • 2
  • Stephen Gilmore
    • 1
  • Maria Luisa Guerriero
    • 1
  • Jane Hillston
    • 1
  1. 1.Centre for Systems Biology at EdinburghThe University of EdinburghEdinburghUK
  2. 2.Laboratory for Foundations of Computer ScienceThe University of EdinburghEdinburghUK

Personalised recommendations