Abstract
We extend the model checking tool MultiVeStA with statistical model checking of steady-state properties. Since MultiVeStA acts as a front-end for simulation tools, it confers this ability onto any tool with which it is integrated. The underlying simulation models are treated as black-box systems. We will use an approach based on batch means using the ASAP3 algorithm. We motivate the work using two case studies: a biochemical model written in the Bio-PEPA language and an application from transport logistics.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Agha, G.A., Meseguer, J., Sen, K.: PMaude: rewrite-based specification language for probabilistic object systems. In: QAPL 2005. ENTCS, vol. 153(2), pp. 213ā239. Elsevier (2006)
Alexopoulos, C., Goldsman, D.: To batch or not to batch? ACM Trans. Model. Comput. Simul. 14(1), 76ā114 (2004)
Alexopoulos, C., Seila, A.F.: Implementing the batch means method in simulation experiments. In: Proceedings of the 28th Conference on Winter Simulation, WSC 1996, pp. 214ā221. IEEE Computer Society, Washington, DC (1996)
AlTurki, M., Meseguer, J.: PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini, A., Klin, B., CĆ®rstea, C. (eds.) CALCO 2011. LNCS, vol. 6859, pp. 386ā392. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22944-2_28
Arora, S., Rathor, A., Rao, M.V.P.: Statistical model checking of opportunistic network protocols. In: Proceedings of AINTEC 2015, pp. 62ā68. ACM (2015)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic (TOCL) 1(1), 162ā170 (2000)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE TSE 29(6), 524ā541 (2003)
Bartoletti, M., Cimoli, T., Murgia, M., Podda, A.S., Pompianu, L.: A contract-oriented middleware. In: Braga, C., Ćlveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 86ā104. Springer, Cham (2016). doi:10.1007/978-3-319-28934-2_5
Belzner, L., Nicola, R., Vandin, A., Wirsing, M.: Reasoning (on) service component ensembles in rewriting logic. In: Iida, S., Meseguer, J., Ogata, K. (eds.) Specification, Algebra, and Software. LNCS, vol. 8373, pp. 188ā211. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54624-2_10
Belzner, L., Hennicker, R., Wirsing, M.: OnPlan: a framework for simulation-based online planning. In: Braga, C., Ćlveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 1ā30. Springer, Cham (2016). doi:10.1007/978-3-319-28934-2_1
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
BuÅ”iÄ, A., Gaujal, B., Vincent, J.-M.: Perfect simulation and non-monotone Markovian systems. In: Valuetools 2008. ICST (2008)
Ciancia, V., Latella, D., Massink, M., PaÅ”kauskas, R., Vandin, A.: A tool-chain for statistical spatio-temporal model checking of bike sharing systems. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 657ā673. Springer, Cham (2016). doi:10.1007/978-3-319-47166-2_46
Ciocchetta, F., Duguid, A., Gilmore, S., Guerriero, M.L., Hillston, J.: The Bio-PEPA tool suite. In: QEST 2009, pp. 309ā310 (2009)
Ciocchetta, F., Duguid, A., Guerriero, M.L.: A compartmental model of the cAMP/PKA/MAPK pathway in Bio-PEPA. In: Ciobanu, G. (ed.) MeCBIC 2009. EPTCS, vol. 11, pp. 71ā90 (2009)
Ciocchetta, F., Hillston, J.: Bio-PEPA: a framework for the modelling and analysis of biological systems. TCS 410(33ā34), 3065ā3084 (2009)
Conway, R.W.: Some tactical problems in digital simulation. Manage. Sci. 10(1), 47ā61 (1963)
Rabih, D., Pekergin, N.: Statistical model checking using perfect simulation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 120ā134. Springer, Heidelberg (2009). doi:10.1007/978-3-642-04761-9_11
Gast, N., Massonnet, G., Reijsbergen, D., Tribastone, M.: Probabilistic forecasts of bike-sharing systems for journey planning. In: CIKM 2015, pp. 703ā712 (2015)
Gilmore, S., Tribastone, M., Vandin, A.: An analysis pathway for the quantitative evaluation of public transport systems. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 71ā86. Springer, Cham (2014). doi:10.1007/978-3-319-10181-1_5
Glynn, P.W., Whitt, W.: The asymptotic validity of sequential stopping rules for stochastic simulations. Ann. Appl. Probab. 2, 180ā198 (1992)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512ā535 (1994)
Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90ā104 (2011)
LāEcuyer, P.: SSJ: Stochastic simulation in Java, software library (2016). http://simul.iro.umontreal.ca/ssj/
LāEcuyer, P., Meliani, L., Vaucher, J.: SSJ: a framework for stochastic simulation in Java. In: YĆ¼cesan, E., Chen, C.-H., Snowdon, J.L., Charnes, J.M. (eds.) Proceedings of the 2002 Winter Simulation Conference, pp. 234ā242. IEEE Press (2002)
Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122ā135. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16612-9_11
Neves, S.R., Tsokas, P., Sarkar, A., Grace, E.A., Rangamani, P., Taubenfeld, S.M., Alberini, C.M., Schaff, J.C., Blitzer, R.D., Moraru, I.I., Iyengar, R.: Cell shape and negative links in regulatory motifs together control spatial information flow in signaling networks. Cell 133(4), 666ā680 (2008)
Pianini, D., Sebastio, S., Vandin, A.: Distributed statistical analysis of complex systems modeled through a chemical metaphor. In: HPCS 2014, pp. 416ā423. IEEE (2014)
Reijsbergen, D., Gilmore, S.: An automated methodology for analysing urban transportation systems using model checking (2016). https://danielreijsbergen.files.wordpress.com/2016/10/bus_modelling1.pdf
Sebastio, S., Amoretti, M., Lluch Lafuente, A.: A computational field framework for collaborative task execution in volunteer clouds. In: SEAMS 2014, pp. 105ā114. ACM (2014)
Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: Valuetools 2013, pp. 310ā315. ACM (2013)
Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202ā215. Springer, Heidelberg (2004). doi:10.1007/978-3-540-27813-9_16
Sen, K., Viswanathan, M., Agha, G.A.: Vesta: a statistical model-checker and analyzer for probabilistic systems. In: QEST 2005, pp. 251ā252 (2005)
Steiger, N.M., Lada, E.K., Wilson, J.R., Joines, J.A., Alexopoulos, C., Goldsman, D.: ASAP3: a batch means procedure for steady-state simulation analysis. ACM Trans. Model. Comput. Simul. 15(1), 39ā73 (2005)
ter Beek, M.H., Legay, A., Lluch-Lafuente, A., Vandin, A.: Statistical analysis of probabilistic models of software product lines with quantitative constraints. In: SPLC 2015, pp. 11ā15. ACM (2015)
ter Beek, M.H., Legay, A., Lluch Lafuente, A., Vandin, A.: Statistical model checking for product lines. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 114ā133. Springer, Cham (2016). doi:10.1007/978-3-319-47166-2_8
Younes, H.L.S.: Probabilistic verification for āBlack-Boxā systems. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 253ā265. Springer, Heidelberg (2005). doi:10.1007/11513988_25
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
Acknowledgments
This work has been supported by the EU project QUANTICOL, 600708. The authors thank Bill Johnston and Philip Lock of Lothian Buses for providing access to the data and for their helpful feedback on parts of this research project, and Jane Hillston for her helpful comments.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
Ā© 2017 Springer International Publishing AG
About this paper
Cite this paper
Gilmore, S., Reijsbergen, D., Vandin, A. (2017). Transient and Steady-State Statistical Analysis for Discrete Event Simulators. In: Polikarpova, N., Schneider, S. (eds) Integrated Formal Methods. IFM 2017. Lecture Notes in Computer Science(), vol 10510. Springer, Cham. https://doi.org/10.1007/978-3-319-66845-1_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-66845-1_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66844-4
Online ISBN: 978-3-319-66845-1
eBook Packages: Computer ScienceComputer Science (R0)