Projects per year
Abstract
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.
Original language | English |
---|---|
Journal | International Journal on Software Tools for Technology Transfer |
Volume | 17 |
Issue number | 3 |
Pages (from-to) | 351-367 |
Number of pages | 17 |
ISSN | 1433-2779 |
DOIs | |
Publication status | Published - 1 Jul 2014 |
Keywords
- statistical model checking
- uppaal
- systems biology
Fingerprint
Dive into the research topics of 'Statistical Model Checking for Biological Systems'. Together they form a unique fingerprint.Projects
- 3 Finished
-
MBAT: Model-based Analysis and Testing of Embedded Systems
Nielsen, B., Larsen, K. G., David, A., Mikucionis, M. & Skou, A.
01/11/2011 → 31/10/2014
Project: Research
-
IDEA4CPS: Foundations for Cyber-Physical Sytems
Larsen, K. G., Skou, A., Nielsen, B., Bulychev, P., Ravn, A. P. & Poulsen, D. B.
01/04/2011 → 30/04/2015
Project: Research
-
MT-LAB: MT-LAB A VKR Foundation Center of Excellence
Larsen, K. G., Skou, A., Srba, J., Ravn, A. P., David, A. & Wisniewski, R.
01/10/2008 → 01/10/2013
Project: Research