Skip to main content
SpringerLink
Log in

Comparative Analysis of Statistical Model Checking Tools

  • Conference paper
  • First Online:
Membrane Computing (CMC 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10105))

Included in the following conference series:

Abstract

Statistical model checking is a powerful and flexible approach for formal verification of computational models, e.g. P systems, which can have very large search spaces. Various statistical model checking tools have been developed, but choosing the most efficient and appropriate tool requires a significant degree of experience, not only because different tools have different modelling and property specification languages, but also because they may be designed to support only a certain subset of property types. Furthermore, their performance can vary depending on the property types and membrane systems being verified. In this paper, we evaluate the performance of various common statistical model checkers based on a pool of biological models. Our aim is to help users select the most suitable SMC tools from among the available options, by comparing their modelling and property specification languages, capabilities and performances.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Alur, R., Henzinger, T.A.: Reactive modules. Form. Methods Syst. Des. 15(1), 7–48 (1999). http://dx.doi.org/10.1023/A:1008739929481

    Article  Google Scholar 

  2. Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time markov chains. ACM Trans. Comput. Logic 1(1), 162–170 (2000). http://doi.acm.org/10.1145/343369.343402

    Article  MathSciNet  Google Scholar 

  3. Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Softw. Eng. 29(6), 524–541 (2003)

    Article  MATH  Google Scholar 

  4. Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  5. Bakir, M.E., Konur, S., Gheorghe, M., Niculescu, I., Ipate, F.: High performance simulations of kernel P systems. In: 2014 IEEE 16th International Conference on High Performance Computing and Communications (HPCC) (2014)

    Google Scholar 

  6. Bakir, M.E., Stannett, M.: Selection criteria for statistical model checking. In: Gheorghe, M., Konur, S. (eds.) Proceedings of the Workshop on Membrane Computing WMC 2016, Manchester (UK), 11–15 July 2016, pp. 55–57 (2016). http://bradscholars.brad.ac.uk/handle/10454/8840, Available as: Technical Report UB-20160819-1, University of Bradford

  7. Bernardini, F., Gheorghe, M., Romero-Campero, F.J., Walkinshaw, N.: A hybrid approach to modeling biological systems. In: Eleftherakis, G., Kefalas, P., Păun, G., Rozenberg, G., Salomaa, A. (eds.) WMC 2007. LNCS, vol. 4860, pp. 138–159. Springer, Heidelberg (2007). doi:10.1007/978-3-540-77312-2_9

    Chapter  Google Scholar 

  8. Blakes, J., Twycross, J., Romero-Campero, F.J., Krasnogor, N.: The infobiotics workbench: An integrated in silico modelling platform for systems and synthetic biology. Bioinformatics 27(23), 3323–3324 (2011)

    Article  Google Scholar 

  9. Blakes, J., Twycross, J., Konur, S., Romero-Campero, F.J., Krasnogor, N., Gheorghe, M.: Infobiotics workbench: A P systems based tool for systems and synthetic biology. In: Frisco, P., Gheorghe, M., Pérez-Jiménez, M.J. (eds.) Applications of Membrane Computing in Systems and Synthetic Biology. Emergence, Complexity and Computation, vol. 7, pp. 1–41. Springer, Heidelberg (2014). doi:10.1007/978-3-319-03191-0_1

    Chapter  Google Scholar 

  10. Bollig-Fischer, A., Marchetti, L., Mitrea, C., Wu, J., Kruger, A., Manca, V., Drăghici, S.: Modeling time-dependent transcription effects of HER2 oncogene and discovery of a role for E2F2 in breast cancer cell-matrix adhesion. Bioinformatics 30(21), 3036–3043 (2014)

    Article  Google Scholar 

  11. Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: A flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D’Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160–164. Springer, Heidelberg (2013). doi:10.1007/978-3-642-40196-1_12

    Chapter  Google Scholar 

  12. Buchholz, P.: A new approach combining simulation and randomization for the analysis of large continuous time Markov chains. ACM Trans. Model Comput. Simul. 8(2), 194–222 (1998). http://doi.acm.org/10.1145/280265.280274

    Article  MATH  Google Scholar 

  13. Carrillo, M., Góngora, P.A., Rosenblueth, D.A.: An overview of existing modeling tools making use of model checking in the analysis of biochemical networks. Front. Plant Sci. 3(155), 1–13 (2012)

    Google Scholar 

  14. Cavaliere, M., Mazza, T., Sedwards, S.: Statistical model checking of membrane systems with peripheral proteins: Quantifying the role of estrogen incellular mitosis and DNA damage. In: Frisco, P., Gheorghe, M., Pérez-Jiménez, M.J. (eds.) Applications of Membrane Computing inSystems and Synthetic Biology. Emergence, Complexity and Computation, vol. 7, pp. 43–63. Springer, Heidelberg (2014). doi:10.1007/978-3-319-03191-0_2

    Chapter  Google Scholar 

  15. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  16. Donaldson, R., Gilbert, D.: A Monte Carlo model checker for Probabilistic LTL with numerical constraints. Technical report, University of Glasgow, Department of Computing Science (2008)

    Google Scholar 

  17. Dragomir, C., Ipate, F., Konur, S., Lefticaru, R., Mierla, L.: Model checking kernel P systems. In: Alhazov, A., Cojocaru, S., Gheorghe, M., Rogozhin, Y., Rozenberg, G., Salomaa, A. (eds.) CMC 2013. LNCS, vol. 8340, pp. 151–172. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54239-8_12

    Chapter  Google Scholar 

  18. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: ICSE 1999, pp. 411–420. ACM, New York (1999)

    Google Scholar 

  19. The European Bioinformatics Institute. http://www.ebi.ac.uk/. Accessed 25 Sept 2016

  20. Fisher, J., Piterman, N.: Model checking in biology. In: Kulkarni, V.V., Stan, G.-B., Raman, K. (eds.) A Systems Theoretic Approach to Systems and Synthetic Biology I Models and System Characterizations, pp. 255–279. Springer, Heidelberg (2014)

    Google Scholar 

  21. Fisher, J., Henzinger, T.A.: Executable cell biology. Nat. Biotech. 25(11), 1239–1249 (2007)

    Article  Google Scholar 

  22. Frisco, P., Gheorghe, M., Pérez-Jiménez, M.J. (eds.): Applications of Membrane Computing in Systems and Synthetic Biology. Emergence, Complexity and Computation, vol. 7. Springer, Heidelberg (2014)

    Google Scholar 

  23. Gheorghe, M., Konur, S., Ipate, F., Mierla, L., Bakir, M.E., Stannett, M.: An integrated model checking toolset for kernel P systems. In: Rozenberg, G., Salomaa, A., Sempere, J.M., Zandron, C. (eds.) CMC 2015. LNCS, vol. 9504, pp. 153–170. Springer, Cham (2015). doi:10.1007/978-3-319-28475-0_11

    Chapter  Google Scholar 

  24. Grunske, L.: Specification patterns for probabilistic quality properties. In: ICSE 2008, pp. 31–40. ACM, New York (2008)

    Google Scholar 

  25. Harel, D.: Statecharts: a visual formalism for complex systems. Sci. Comput. Program. 8(3), 231–274 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  26. Heiner, M., Gilbert, D., Donaldson, R.: Petri nets for systems and synthetic biology. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 215–264. Springer, Heidelberg (2008). doi:10.1007/978-3-540-68894-5_7

    Chapter  Google Scholar 

  27. Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 441–444. Springer, Heidelberg (2006). doi:10.1007/11691372_29

    Chapter  Google Scholar 

  28. Huth, M., Ryan, M.: Logic in Computer Science: Modelling and Reasoning about Systems, 2nd edn. Cambridge University Press, Cambridge (2004)

    Book  MATH  Google Scholar 

  29. Katoen, J.P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. In: Quantitative Evaluation of Systems (QEST), pp. 167–176. IEEE Computer Society (2009)

    Google Scholar 

  30. Kauffman, S.A.: Metabolic stability and epigenesis in randomly constructed genetic nets. J. Theoret. Biol. 22, 437–467 (1969)

    Article  MathSciNet  Google Scholar 

  31. Konur, S., Gheorghe, M.: A property-driven methodology for formal analysis of synthetic biology systems. IEEE/ACM Trans. Comput. Biol. Bioinform. 12(2), 360–371 (2015)

    Article  Google Scholar 

  32. kPWorkbench. http://kpworkbench.org/. Accessed 25 Sept 2016

  33. Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 200–204. Springer, Heidelberg (2002). doi:10.1007/3-540-46029-2_13

    Chapter  Google Scholar 

  34. Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol. 4486, pp. 220–270. Springer, Heidelberg (2007). doi:10.1007/978-3-540-72522-0_6

    Chapter  Google Scholar 

  35. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: An overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16612-9_11

    Chapter  Google Scholar 

  36. Lindenmayer, A., Jürgensen, H.: Grammars of development: Discrete-state models for growth, differentiation, and gene expression in modular organisms. In: Rozenberg, G., Salomaa, A. (eds.) Lindenmayer Systems: Impacts on Theoretical Computer Science, Computer Graphics, and Developmental Biology, pp. 3–21. Springer, Heidelberg (1992). doi:10.1007/978-3-642-58117-5_1

    Chapter  Google Scholar 

  37. Manca, V.: Infobiotics: Information in Biotic Systems. Emergence, Complexity and Computation, vol. 3. Springer, Heidelberg (2013)

    MATH  Google Scholar 

  38. Milner, R.: Communicating and Mobile Systems: The Pi-Calculus. Cambridge University Press, New York (1999)

    MATH  Google Scholar 

  39. Monteiro, P.T., Ropers, D., Mateescu, R., Freitas, A.T., de Jong, H.: Temporal logic patterns for querying dynamic models of cellular interaction networks. Bioinformatics 24(16), i227–i233 (2008). http://dx.doi.org/10.1093/bioinformatics/btn275

    Article  Google Scholar 

  40. Markow Reward Model Checker (MRMC). http://www.mrmc-tool.org/. Accessed 18 Feb 2015

  41. Pérez-Jiménez, M.J., Romero-Campero, F.J.: P systems, a new computational modelling tool for systems biology. In: Priami, C., Plotkin, G. (eds.) Transactions on Computational Systems Biology VI. LNCS, vol. 4220, pp. 176–197. Springer, Heidelberg (2006). doi:10.1007/11880646_8

    Chapter  Google Scholar 

  42. Plasma-Lab. https://project.inria.fr/plasma-lab/. Accessed 18 Feb 2015

  43. Reisig, W.: The basic concepts. In: Understanding Petri Nets: Modeling Techniques, Analysis Methods, Case Studies, pp. 13–24. Springer, Heidelberg (2013). http://dx.doi.org/10.1007/978-3-642-33278-4_2

  44. Probabilistic and Symbolic Model Checker (PRISM). http://www.prismmodelchecker.org/. Accessed 08 Jan 2015

  45. Sanassy, D., Widera, P., Krasnogor, N.: Meta-stochastic simulation of biochemical models for systems and synthetic biology. ACS Synth. Biol. 4(1), 39–47 (2015). pMID: 25152014. http://dx.doi.org/10.1021/sb5001406

    Article  Google Scholar 

  46. Ymer website. http://www.tempastic.org/ymer/. Accessed 25 Aug 2015

  47. Younes, H., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Technol. Transfer (STTT) 8(3), 216–228 (2006)

    Article  MATH  Google Scholar 

  48. Younes, H.L.S.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429–433. Springer, Heidelberg (2005). doi:10.1007/11513988_43

    Chapter  Google Scholar 

  49. Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 223–235. Springer, Heidelberg (2002). doi:10.1007/3-540-45657-0_17

    Chapter  Google Scholar 

  50. Zapreev, I.S., Jansen, C.: Markov reward model checker manual. http://www.mrmc-tool.org/downloads/MRMC/Specs/MRMC_Manual.pdf

  51. Zuliani, P.: Statistical model checking for biological applications. Int. J. Softw. Tools Technol. Transfer 17(4), 527–536 (2014). http://dx.doi.org/10.1007/s10009-014-0343-0

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The University of Sheffield, Regent Court, 211 Portobello, Sheffield, S1 4DP, UK

    Mehmet Emin Bakir & Mike Stannett

  2. School of Electrical Engineering and Computer Science, University of Bradford, West Yorkshire, Bradford, BD7 1DP, UK

    Marian Gheorghe & Savas Konur

Authors
  1. Mehmet Emin Bakir
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marian Gheorghe
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Savas Konur
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mike Stannett
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mehmet Emin Bakir .

Editor information

Editors and Affiliations

  1. University of Milano-Bicocca , Milan, Italy

    Alberto Leporati

  2. Leiden University , Leiden, The Netherlands

    Grzegorz Rozenberg

  3. Turku Center for Computer Science , Turku, Finland

    Arto Salomaa

  4. University of Milan-Bicocca , Milan, Italy

    Claudio Zandron

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Bakir, M.E., Gheorghe, M., Konur, S., Stannett, M. (2017). Comparative Analysis of Statistical Model Checking Tools. In: Leporati, A., Rozenberg, G., Salomaa, A., Zandron, C. (eds) Membrane Computing. CMC 2016. Lecture Notes in Computer Science(), vol 10105. Springer, Cham. https://doi.org/10.1007/978-3-319-54072-6_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-54072-6_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-54071-9

  • Online ISBN: 978-3-319-54072-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation