Skip to main content
SpringerLink
Log in

Probabilistic Black-Box Reachability Checking

  • Conference paper
  • First Online:
Runtime Verification (RV 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10548))

Included in the following conference series:

Abstract

Model checking has a long-standing tradition in software verification. Given a system design it checks whether desired properties are satisfied. Unlike testing, it cannot be applied in a black-box setting. To overcome this limitation Peled et al.  introduced black-box checking, a combination of testing, model inference and model checking. The technique requires systems to be fully deterministic. For stochastic systems, statistical techniques are available. However, they cannot be applied to systems with non-deterministic choices. We present a black-box checking technique for stochastic systems that allows both, non-deterministic and probabilistic behaviour. It involves model inference, testing and probabilistic model-checking. Here, we consider reachability checking, i.e., we infer near-optimal input-selection strategies for bounded reachability.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Aichernig, B.K., Tappler, M.: Learning from faults: mutation testing in active automata learning. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 19–34. Springer, Cham (2017). doi:10.1007/978-3-319-57288-8_2

    Chapter  Google Scholar 

  2. Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987). doi:10.1016/0890-5401(87)90052-6

    Article  MathSciNet  MATH  Google Scholar 

  3. Banks, A., Gupta, R. (eds.): MQTT Version 3.1.1. OASIS Standard, October 2014. http://docs.oasis-open.org/mqtt/mqtt/v3.1.1/os/mqtt-v3.1.1-os.html, latest version. http://docs.oasis-open.org/mqtt/mqtt/v3.1.1/os/mqtt-v3.1.1-os.html

  4. Brázdil, T., Chatterjee, K., Chmelik, M., Forejt, V., Kretínský, J., Kwiatkowska, M.Z., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: Cassez and Raskin [6], pp. 98–114. http://dx.doi.org/10.1007/978-3-319-11936-6_8

  5. Carrasco, R.C., Oncina, J.: Learning stochastic regular grammars by means of a state merging method. In: Carrasco, R.C., Oncina, J. (eds.) ICGI 1994. LNCS, vol. 862, pp. 139–152. Springer, Heidelberg (1994). doi:10.1007/3-540-58473-0_144

    Chapter  Google Scholar 

  6. Cassez, F., Raskin, J.-F. (eds.): ATVA 2014. LNCS, vol. 8837. Springer, Cham (2014)

    MATH  Google Scholar 

  7. Chen, Y., Nielsen, T.D.: Active learning of Markov decision processes for system verification. In: 11th International Conference on Machine Learning and Applications, ICMLA, Boca Raton, FL, USA, December 12–15, 2012, vol. 2, pp. 289–294. IEEE (2012). http://dx.doi.org/10.1109/ICMLA.2012.158

  8. D’Argenio, P., Legay, A., Sedwards, S., Traonouez, L.: Smart sampling for lightweight verification of Markov decision processes. STTT 17(4), 469–484 (2015). doi:10.1007/s10009-015-0383-0

    Article  Google Scholar 

  9. David, A., Jensen, P.G., Larsen, K.G., Legay, A., Lime, D., Sørensen, M.G., Taankvist, J.H.: On time with minimal expected cost!. In: Cassez and Raskin [6], pp. 129–145. http://dx.doi.org/10.1007/978-3-319-11936-6_10

  10. David, A., Jensen, P.G., Larsen, K.G., Mikučionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206–211. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_16

    Google Scholar 

  11. Elkind, E., Genest, B., Peled, D., Qu, H.: Grey-box checking. In: Najm, E., Pradat-Peyre, J.-F., Donzeau-Gouge, V.V. (eds.) FORTE 2006. LNCS, vol. 4229, pp. 420–435. Springer, Heidelberg (2006). doi:10.1007/11888116_30

    Chapter  Google Scholar 

  12. EMQ. http://emqtt.io/. Accessed 07 May 2017

  13. Fiterău-Broştean, P., Janssen, R., Vaandrager, F.: Combining model learning and model checking to analyze TCP implementations. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 454–471. Springer, Cham (2016). doi:10.1007/978-3-319-41540-6_25

    Google Scholar 

  14. Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 53–113. Springer, Heidelberg (2011). doi:10.1007/978-3-642-21455-4_3

    Chapter  Google Scholar 

  15. Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 357–370. Springer, Heidelberg (2002). doi:10.1007/3-540-46002-0_25

    Chapter  Google Scholar 

  16. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_47

    Chapter  Google Scholar 

  17. Kwiatkowska, M., Parker, D.: Automated verification and strategy synthesis for probabilistic systems. In: Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 5–22. Springer, Cham (2013). doi:10.1007/978-3-319-02444-8_2

    Chapter  Google Scholar 

  18. Larsen, K.G., Legay, A.: Statistical model checking: past, present, and future. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 3–15. Springer, Cham (2016). doi:10.1007/978-3-319-47166-2_1

    Chapter  Google Scholar 

  19. Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). doi:10.1007/978-3-642-16612-9_11

    Chapter  Google Scholar 

  20. Legay, A., Sedwards, S., Traonouez, L.-M.: Scalable verification of Markov decision processes. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 350–362. Springer, Cham (2015). doi:10.1007/978-3-319-15201-1_23

    Google Scholar 

  21. Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning probabilistic automata for model checking. In: Eighth International Conference on Quantitative Evaluation of Systems, QEST 2011, Aachen, Germany, 5–8, pp. 111–120. IEEE Computer Society (2011). http://dx.doi.org/10.1109/QEST.2011.21

  22. Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning Markov decision processes for model checking. In: Fahrenberg, U., Legay, A., Thrane, C.R. (eds.) Proceedings Quantities in Formal Methods, QFM 2012, Paris, France, 28. EPTCS, vol. 103, pp. 49–63 (2012). http://dx.doi.org/10.4204/EPTCS.103.6

  23. Mao, H., Chen, Y., Jaeger, M., Nielsen, T.D., Larsen, K.G., Nielsen, B.: Learning deterministic probabilistic automata from a model checking perspective. Mach. Learn. 105(2), 255–299 (2016). doi:10.1007/s10994-016-5565-9

    Article  MathSciNet  Google Scholar 

  24. Nachmanson, L., Veanes, M., Schulte, W., Tillmann, N., Grieskamp, W.: Optimal strategies for testing nondeterministic systems. In: Avrunin, G.S., Rothermel, G. (eds.) Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2004, Boston, Massachusetts, USA, July 11–14, 2004, pp. 55–64. ACM (2004). http://doi.acm.org/10.1145/1007512.1007520

  25. Nouri, A., Raman, B., Bozga, M., Legay, A., Bensalem, S.: Faster statistical model checking by means of abstraction and learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 340–355. Springer, Cham (2014). doi:10.1007/978-3-319-11164-3_28

    Google Scholar 

  26. Okamoto, M.: Some inequalities relating to the partial sum of binomial probabilities. Ann. Inst. Stat. Math. 10(1), 29–35 (1959). doi:10.1007/BF02883985

    Article  MathSciNet  MATH  Google Scholar 

  27. Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Formal Methods for Protocol Engineering and Distributed Systems. IAICT, vol. 28, pp. 225–240. Springer, Boston, MA (1999). doi:10.1007/978-0-387-35578-8_13

    Chapter  Google Scholar 

  28. prob-black-reach - Java implementation of probabilistic black-box reachability checking. https://github.com/mtappler/prob-black-reach. Accessed 07 May 2017

  29. 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

    Chapter  Google Scholar 

  30. Shu, G., Lee, D.: Testing security properties of protocol implementations - a machine learning based approach. In: 27th IEEE International Conference on Distributed Computing Systems (ICDCS 2007), June 25–29, 2007, Toronto, Ontario, Canada, p. 25. IEEE Computer Society (2007). http://dx.doi.org/10.1109/ICDCS.2007.147

  31. Tappler, M., Aichernig, B.K., Bloem, R.: Model-based testing IoT communication via active automata learning. In: ICST 2017, pp. 276–287. IEEE Computer Society (2017)

    Google Scholar 

  32. TCP models. https://gitlab.science.ru.nl/pfiteraubrostean/tcp-learner/tree/cav-aec/models. Accessed 07 May 2017

  33. Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Softw. Test., Verif. Reliab. 22(5), 297–312 (2012). doi:10.1002/stvr.456

    Article  Google Scholar 

  34. Verwer, S., Weerdt, M., Witteveen, C.: A likelihood-ratio test for identifying probabilistic deterministic real-time automata from positive data. In: Sempere, J.M., García, P. (eds.) ICGI 2010. LNCS (LNAI), vol. 6339, pp. 203–216. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15488-1_17

    Chapter  Google Scholar 

  35. Wang, J., Sun, J., Qin, S.: Verifying complex systems probabilistically through learning, abstraction and refinement. CoRR abs/1610.06371 (2016). http://arxiv.org/abs/1610.06371

  36. 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

    Chapter  Google Scholar 

Download references

Acknowledgment

This work was supported by the TU Graz LEAD project “Dependable Internet of Things in Adverse Environments”. The authors would like to thank the LEAD project members Roderick Bloem, Masoud Ebrahimi, Franz Pernkopf, Franz Röck, and Tobias Schrank for fruitful discussions.

Author information

Authors and Affiliations

  1. Institute of Software Technology, Graz University of Technology, Graz, Austria

    Bernhard K. Aichernig & Martin Tappler

Authors
  1. Bernhard K. Aichernig
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martin Tappler
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Martin Tappler .

Editor information

Editors and Affiliations

  1. Microsoft Research, Redmond, Washington, USA

    Shuvendu Lahiri

  2. The University of Manchester, Manchester, United Kingdom

    Giles Reger

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Aichernig, B.K., Tappler, M. (2017). Probabilistic Black-Box Reachability Checking. In: Lahiri, S., Reger, G. (eds) Runtime Verification. RV 2017. Lecture Notes in Computer Science(), vol 10548. Springer, Cham. https://doi.org/10.1007/978-3-319-67531-2_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67531-2_4

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67530-5

  • Online ISBN: 978-3-319-67531-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation