Advertisement

Transient and Steady-State Statistical Analysis for Discrete Event Simulators

  • Stephen Gilmore
  • Daniël Reijsbergen
  • Andrea VandinEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)

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.

Keywords

Statistical model checking Steady-state Batch means MultiVeStA 

Notes

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.

References

  1. 1.
    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)Google Scholar
  2. 2.
    Alexopoulos, C., Goldsman, D.: To batch or not to batch? ACM Trans. Model. Comput. Simul. 14(1), 76–114 (2004)CrossRefGoogle Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    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 CrossRefGoogle Scholar
  5. 5.
    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)Google Scholar
  6. 6.
    Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic (TOCL) 1(1), 162–170 (2000)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE TSE 29(6), 524–541 (2003)zbMATHGoogle Scholar
  8. 8.
    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 CrossRefGoogle Scholar
  9. 9.
    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 CrossRefGoogle Scholar
  10. 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 CrossRefGoogle Scholar
  11. 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 CrossRefGoogle Scholar
  12. 12.
    Bušić, A., Gaujal, B., Vincent, J.-M.: Perfect simulation and non-monotone Markovian systems. In: Valuetools 2008. ICST (2008)Google Scholar
  13. 13.
    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 CrossRefGoogle Scholar
  14. 14.
    Ciocchetta, F., Duguid, A., Gilmore, S., Guerriero, M.L., Hillston, J.: The Bio-PEPA tool suite. In: QEST 2009, pp. 309–310 (2009)Google Scholar
  15. 15.
    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)Google Scholar
  16. 16.
    Ciocchetta, F., Hillston, J.: Bio-PEPA: a framework for the modelling and analysis of biological systems. TCS 410(33–34), 3065–3084 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Conway, R.W.: Some tactical problems in digital simulation. Manage. Sci. 10(1), 47–61 (1963)MathSciNetCrossRefGoogle Scholar
  18. 18.
    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 CrossRefGoogle Scholar
  19. 19.
    Gast, N., Massonnet, G., Reijsbergen, D., Tribastone, M.: Probabilistic forecasts of bike-sharing systems for journey planning. In: CIKM 2015, pp. 703–712 (2015)Google Scholar
  20. 20.
    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 Google Scholar
  21. 21.
    Glynn, P.W., Whitt, W.: The asymptotic validity of sequential stopping rules for stochastic simulations. Ann. Appl. Probab. 2, 180–198 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512–535 (1994)CrossRefzbMATHGoogle Scholar
  23. 23.
    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)CrossRefGoogle Scholar
  24. 24.
    L’Ecuyer, P.: SSJ: Stochastic simulation in Java, software library (2016). http://simul.iro.umontreal.ca/ssj/
  25. 25.
    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)Google Scholar
  26. 26.
    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 CrossRefGoogle Scholar
  27. 27.
    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)CrossRefGoogle Scholar
  28. 28.
    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)Google Scholar
  29. 29.
    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
  30. 30.
    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)Google Scholar
  31. 31.
    Sebastio, S., Vandin, A.: MultiVeStA: statistical model checking for discrete event simulators. In: Valuetools 2013, pp. 310–315. ACM (2013)Google Scholar
  32. 32.
    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 CrossRefGoogle Scholar
  33. 33.
    Sen, K., Viswanathan, M., Agha, G.A.: Vesta: a statistical model-checker and analyzer for probabilistic systems. In: QEST 2005, pp. 251–252 (2005)Google Scholar
  34. 34.
    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)CrossRefGoogle Scholar
  35. 35.
    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)Google Scholar
  36. 36.
    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 CrossRefGoogle Scholar
  37. 37.
    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 CrossRefGoogle Scholar
  38. 38.
    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 CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Stephen Gilmore
    • 1
  • Daniël Reijsbergen
    • 1
  • Andrea Vandin
    • 2
    Email author
  1. 1.University of EdinburghEdinburghScotland
  2. 2.IMT School for Advanced StudiesLuccaItaly

Personalised recommendations