nach oben

International Journal on Software Tools for Technology Transfer

Erschienen in:

01.06.2015 | Regular Paper

Statistical model checking for biological systems

verfasst von: Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen, Sean Sedwards

Erschienen in: International Journal on Software Tools for Technology Transfer | Ausgabe 3/2015

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Vorheriger Artikel Incremental test case generation using bounded model checking: an application to automatic rating

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

http://www.mathworks.se/products/simbiology/.

http://www.danse-ip.eu/home/.

http://www.idea4cps.dk/.

In fact the colouring of the nodes represent how large a fraction of each species is active.

http://sbml.org.

http://www.ebi.ac.uk/biomodels-main/publmodels.

They can be added to the CTMC model as well but this is not yet implemented.

The individual scaling or simulation steps are not reported here for brevity.

e.g. StateSpace approach is not applicable due to multiple species coupling.

Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci 126(2), 183–235 (1994). doi:10.1016/0304-3975(94)90010-8 CrossRefMATHMathSciNet

Barkai, N., Leibler, S.: Biological rhythms: circadian clocks limited by noise. Nature 403, 267–268 (2000)

Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. In: Hatcliff, J., Zucca, E. (eds.) Formal Techniques for Distributed Systems, vol. 6117 of Lecture Notes in Computer Science, pp. 32–46. Springer, Berlin (2010). ISBN: 978-3-642-13463-0. doi:10.1007/978-3-642-13464-74

Behrmann, G., David, A., Larsen, K.G.: A Tutorial on Uppaal. Lecture Notes in Computer Science, pp. 200–236 (2004)

Behrmann, Gerd, David, Alexandre, Larsen, Kim Guldstrand, Pettersson, Paul, Yi, Wang: Developing UPPAAL over 15 years. Softw. Pract. Exper 41(2), 133–142 (2011). doi:10.1002/spe.1006 CrossRef

Bergmann, F.T., Sauro, H.M.: Comparing simulation results of SBML capable simulators. Bioinformatics 24(17):1963–1965 (2008). doi:10.1093/bioinformatics/btn319. URL: http://bioinformatics.oxfordjournals.org/content/24/17/1963.full

Bulychev, P., David, A., Larsen, K.G., Legay, A., Mikučionis, M.: Computing Nash Equilibrium in Wireless Ad Hoc Networks: A Simulation-Based Approach. In: Reich, J., Finkbeiner, B. (eds.) Second International Workshop on Interactions, Games and Protocols, vol. 78 of EPTCS, pp. 1–14 (2012). doi:10.4204/EPTCS.78

Bulychev, P.E., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-Based Statistical Model Checking of WMTL. In: Qadeer S., Tasiran, S. (ed.) RV, vol. 7687 of Lecture Notes in Computer Science, pp. 260–275. Springer, Berlin (2012). ISBN: 978-3-642-35631-5-642-35632-2. doi:10.1007/978-3-642-35632-225

Bulychev, P.E., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B., Stainer, A.: Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic. In: Bjørner, N., Voronkov, A. (eds.) LPAR, vol. 7180 of Lecture Notes in Computer Science, pp. 168–182. Springer, Berlin (2012). ISBN:978-3-642-28716-9. doi:10.1007/978-3-642-28717-615

10.

David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., van Vliet, J., Wang, Z.: Statistical Model Checking for Networks of Priced Timed Automata. In: Fahrenberg, U., Tripakis, S. (eds.) FORMATS, vol. 6919 of Lecture Notes in Computer Science, pp. 80–96. Springer, Berlin (2011). ISBN:978-3-642-24309-7. doi:10.1007/978-3-642-24310-37

11.

David, A., Du, D., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Sedwards, S.: Statistical Model Checking for Stochastic Hybrid Systems. In: Bartocci, E., Bortolussi, L. (eds.) HSB, vol. 92 of EPTCS, pp. 122–136 (2012). doi:10.4204/EPTCS.92.9

12.

David, A., Du, D., Larsen, K.G., Mikučionis, M., Skou, A.: An evaluation framework for energy aware buildings using statistical model checking. Sci. China Inform. Sci. 55:2694–2707, 2012. ISSN:1674–733X. doi:10.1007/s11432-012-4742-0. URL:http://dx.doi.org/10.1007/s11432-012-4742-0

13.

David, A., Larsen, K.G., Legay, A., Mikučionis, M.: Schedulability of Herschel-Planck Revisited Using Statistical Model Checking. In: Margaria, T., Steffen, B. (eds.) ISoLA (2), vol. 7610 of Lecture Notes in Computer Science, pp. 293–307. Springer, Berlin (2012). ISBN:978-3-642-34031-4. doi:10.1007/978-3-642-34032-128

14.

David, A., Larsen, K.G., Legay, A., Mikučionis, M., Poulsen, D.B., Sedwards, S.: Runtime Verification of Biological Systems. In: ISoLA (1), pp. 388–404 (2012). doi:10.1007/978-3-642-34026-029

15.

Faeder, J.R., Blinov, M.L., Hlavacek, W.S.: Rule-based modeling of biochemical systems with BioNetGen. Syst. Biol. 500 (2009). doi:10.1007/978-1-59745-525-15

16.

Gillespie, D.T.: Exact stochastic simulation of coupled chemical reactions. J. Phys. Chem. 81:2340–2361 (1977). doi:10.1021/j100540a008

17.

Hilborn, R.C., Erwin, J.D.: Stochastic coherence in an oscillatory gene circuit model. J. Theor. Biol. 253(2):349–354 (2008). ISSN:0022–5193. doi:10.1016/j.jtbi.2008.03.012. URL:http://www.sciencedirect.com/science/article/pii/S0022519308001264

18.

Jegourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking—PLASMA. In: Flanagan, C., König, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, vol. 7214 of Lecture Notes in Computer Science, pp. 498–503. Springer, Berlin (2012). ISBN:978-3-642-28755-8. doi:10.1007/978-3-642-28756-537

19.

Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. STTT 1(1—-2), 134–152 (1997). doi:10.1007/s100090050010 CrossRefMATH

20.

Legay, A., Delahaye, B., Bensalem, S.: Statistical Model Checking: An Overview. In: RV, vol. 6418 of Lecture Notes in Computer Science, pp. 122–135. Springer, Berlin (2010). doi:10.1007/978-3-642-16612-911

21.

Schivo, S., Scholma, J., Wanders, B., Urquidi Camacho, R.A., van der Vet, P.E., Karperien, M., Langerak, R., van de Pol, J., Post, J.N.: Modelling biological pathway dynamics with Timed Automata. IEEE J. Biomed. Health Inform. PP(99):1–1 (2013). ISSN:2168–2194. doi:10.1109/JBHI.2013.2292880

22.

Schivo, S., Scholma, J., Wanders, B., Urquidi C., Ricardo A., van der Vet, Paul E., Karperien, M., Langerak, R., van de Pol, J., Post, J.N.: Modelling biological pathway dynamics with Timed Automata. In: Proceedings of the 2012 IEEE 12th International Conference on Bioinformatics and Bioengineering (BIBE), pp. 447–453 (2012)

23.

Sen, K., Viswanathan, M., Agha, G.: Statistical Model Checking of Black-Box Probabilistic Systems. In: CAV, LNCS 3114, pp. 202–215. Springer, Berlin (2004). doi:10.1007/978-3-540-27813-916

24.

Shannon, P., Markiel, A., Ozier, O., Amin, N., Schwikowski, Benno, Ideker, Trey: Cytoscape: a software environment for integrated models of biomolecular interaction networks. Genome Res. 13(11), 2498–2504 (2003). doi:10.1101/gr.1239303 CrossRef

25.

Vilar, J.M.G., Kueh, H.Y., Barkai, N., Leibler, S.: Mechanisms of noise-resistance in genetic oscillators. Proc. Natl. Acad. Sci. 99(9): 5988–5992, 2002. doi:10.1073/pnas.092133899. URL http://www.pnas.org/content/99/9/5988.abstract

26.

Younes, H.L.S., Simmons, R.G.: Probabilistic Verification of Discrete Event Systems Using Acceptance Sampling. In: Proceeding of 14th International Conference on Computer Aided Verification (CAV), LNCS 2404, pp. 223–235. Springer, Berlin (2002)

27.

Younes, H.L.S.: Ymer: A Statistical Model Checker. In: Etessami, K., Rajamani, S.K. (eds.) Computer Aided Verification, vol. 3576 of Lecture Notes in Computer Science, pp. 429–433. Springer, Berlin (2005). ISBN:978-3-540-27231-1. doi:10.1007/1151398843

Titel: Statistical model checking for biological systems
verfasst von: Alexandre David
Kim G. Larsen
Axel Legay
Marius Mikučionis
Danny Bøgsted Poulsen
Sean Sedwards
Publikationsdatum: 01.06.2015
Verlag: Springer Berlin Heidelberg
Erschienen in: International Journal on Software Tools for Technology Transfer / Ausgabe 3/2015
Print ISSN: 1433-2779
Elektronische ISSN: 1433-2787
DOI: https://doi.org/10.1007/s10009-014-0323-4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Weitere Artikel der Ausgabe 3/2015

Security risk analysis of system changes exemplified within the oil and gas domain

Policy ignorant caller-side inline reference monitoring

Restoring security of evolving software models using graph transformation

A process for mastering security evolution in the development lifecycle

A systematic classification of security regression testing approaches

Incremental test case generation using bounded model checking: an application to automatic rating