Statistical model checking for biological systems

Statistical Model Checking (SMC) is a highly scalable simulation-based verification approach for testing and estimating the probability that a stochastic system satisfies a given linear temporal property. The technique has been applied to (discrete and continuous time) Markov chains, stochastic timed automata and most recently hybrid systems using the tool Uppaal SMC. In this paper we enable the application of SMC to complex biological systems, by combining Uppaal SMC with ANIMO, a plugin of the tool Cytoscape used by biologists, as well as with SimBiology®, a plugin of Matlab to simulate reactions. ANIMO and SimBiology® are two domain specific tools that have their own user interfaces and formalisms specifically tailored towards the biology domain. However—though providing means for simulation—both tools lack the powerful analytic capabilities offered by SMC, which in previous work have proved very useful for identifying interesting properties of biological systems. Our aim is to offer the best of the two worlds: optimal domain specific interfaces and formalisms suited to biology combined with powerful SMC analysis techniques for stochastic and hybrid systems. This goal is obtained by developing translators from the XGMML and SBML formats used by Cytoscape and SimBiology® to stochastic and hybrid automata, allowing Uppaal SMC to be used as an efficient backend analysis tool, that we demonstrate can handle real-world biological systems by pitting it against the BioModels database. We present detailed analysis on two particular case-studies involving the ANIMO and SimBiology® tools.