×

Probabilistic black-box reachability checking (extended version). (English) Zbl 1425.68247

Summary: 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.

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aichernig, Bernhard K.; Mostowski, Wojciech; Mousavi, Mohammad Reza; Tappler, Martin; Taromirad, Masoumeh, Model Learning and Model-Based Testing, 74-100 (2018), Cham
[2] Aichernig, Bernhard K.; Tappler, Martin, Learning from Faults: Mutation Testing in Active Automata Learning, 19-34 (2017), Cham
[3] Aichernig, Bernhard K.; Tappler, Martin, Probabilistic Black-Box Reachability Checking, 50-67 (2017), Cham · Zbl 1425.68247 · doi:10.1007/978-3-319-67531-2_4
[4] Angluin, D., Learning regular sets from queries and counterexamples, Inf. Comput., 75, 87-106 (1987) · Zbl 0636.68112 · doi:10.1016/0890-5401(87)90052-6
[5] Argyros G, Stais I, Jana S, Keromytis AD, Kiayias A (2016) SFADiff: automated evasion attacks and fingerprinting using black-box differential automata learning. In: Proceedings of the 2016 ACM SIGSAC conference on computer and communications security, pp 1690-1701. ACM. https://doi.org/10.1145/2976749.2978383
[6] Aspnes, J.; Herlihy, M., Fast randomized consensus using shared memory, J Algorithms, 11, 441-461 (1990) · Zbl 0705.68016 · doi:10.1016/0196-6774(90)90021-6
[7] Baier C, Katoen J (2008) Principles of model checking. MIT Press, Cambridge · Zbl 1179.68076
[8] Banks A. Gupta, R (ed.) (2014) MQTT version 3.1.1. OASIS standard. http://docs.oasis-open.org/mqtt/mqtt/v3.1.1/os/mqtt-v3.1.1-os.html. http://docs.oasis-open.org/mqtt/mqtt/v3.1.1/os/mqtt-v3.1.1-os.html
[9] Beimel, A.; Bergadano, F.; Bshouty, NH; Kushilevitz, E.; Varricchio, S., Learning functions represented as multiplicity automata, J ACM, 47, 506-530 (2000) · Zbl 1094.68575 · doi:10.1145/337244.337257
[10] Brázdil, Tomáš; Chatterjee, Krishnendu; Chmelík, Martin; Forejt, Vojtěch; Křetínský, Jan; Kwiatkowska, Marta; Parker, David; Ujma, Mateusz, Verification of Markov Decision Processes Using Learning Algorithms, 98-114 (2014), Cham · Zbl 1448.68290 · doi:10.1007/978-3-319-11936-6_8
[11] Carrasco, Rafael C.; Oncina, Jose, Learning stochastic regular grammars by means of a state merging method, 139-152 (1994), Berlin, Heidelberg · doi:10.1007/3-540-58473-0_144
[12] Cassez F, Raskin J (eds) (2014) Automated technology for verification and analysis-12th international symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014. Proceedings, Lecture notes in computer science, vol 8837. Springer. https://doi.org/10.1007/978-3-319-11936-6 · Zbl 1325.68014
[13] Chen Y, Nielsen TD (2012) 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. https://doi.org/10.1109/ICMLA.2012.158
[14] D’Argenio, P.; Legay, A.; Sedwards, S.; Traonouez, L., Smart sampling for lightweight verification of Markov decision processes, STTT, 17, 469-484 (2015) · doi:10.1007/s10009-015-0383-0
[15] David, Alexandre; Jensen, Peter G.; Larsen, Kim Guldstrand; Legay, Axel; Lime, Didier; Sørensen, Mathias Grund; Taankvist, Jakob H., On Time with Minimal Expected Cost!, 129-145 (2014), Cham · Zbl 1448.68294 · doi:10.1007/978-3-319-11936-6_10
[16] David, Alexandre; Jensen, Peter Gjøl; Larsen, Kim Guldstrand; Mikučionis, Marius; Taankvist, Jakob Haahr, Uppaal Stratego, 206-211 (2015), Berlin, Heidelberg · doi:10.1007/978-3-662-46681-0_16
[17] Elkind, Edith; Genest, Blaise; Peled, Doron; Qu, Hongyang, Grey-Box Checking, 420-435 (2006), Berlin, Heidelberg · Zbl 1225.68113
[18] EMQ. http://emqtt.io/. Accessed 3 Dec 2018
[19] Feng, Lu; Han, Tingting; Kwiatkowska, Marta; Parker, David, Learning-Based Compositional Verification for Synchronous Probabilistic Systems, 511-521 (2011), Berlin, Heidelberg · Zbl 1348.68135 · doi:10.1007/978-3-642-24372-1_40
[20] Fiterău-Broştean, Paul; Janssen, Ramon; Vaandrager, Frits, Combining Model Learning and Model Checking to Analyze TCP Implementations, 454-471 (2016), Cham · doi:10.1007/978-3-319-41540-6_25
[21] Fiterau-Brostean P, Lenaerts T, Poll E, de Ruiter J, Vaandrager FW, Verleg P (2017) Model learning and model checking of SSH implementations. In: Erdogmus H, Havelund K (eds) Proceedings of the 24th ACM SIGSOFT international SPIN symposium on model checking of software, Santa Barbara, CA, July 10-14, 2017, pp 142-151. ACM. https://doi.org/10.1145/3092282.3092289. http://doi.acm.org/10.1145/3092282.3092289
[22] Forejt, Vojtěch; Kwiatkowska, Marta; Norman, Gethin; Parker, David, Automated Verification Techniques for Probabilistic Systems, 53-113 (2011), Berlin, Heidelberg · Zbl 1315.68177 · doi:10.1007/978-3-642-21455-4_3
[23] Fu J, Topcu U (2014) Probably approximately correct MDP learning and control with temporal logic constraints. In: Fox D, Kavraki LE, Kurniawati H (eds) Robotics: science and systems X, University of California, Berkeley, July 12-16, 2014. http://www.roboticsproceedings.org/rss10/p39.html
[24] Giantamidis, Georgios; Tripakis, Stavros, Learning Moore Machines from Input-Output Traces, 291-309 (2016), Cham · Zbl 1427.68133 · doi:10.1007/978-3-319-48989-6_18
[25] Grinchtein, Olga; Jonsson, Bengt; Leucker, Martin, Learning of Event-Recording Automata, 379-395 (2004), Berlin, Heidelberg · Zbl 1109.68515 · doi:10.1007/978-3-540-30206-3_26
[26] Groce, Alex; Peled, Doron; Yannakakis, Mihalis, Adaptive Model Checking, 357-370 (2002), Berlin, Heidelberg · Zbl 1043.68570 · doi:10.1007/3-540-46002-0_25
[27] de la Higuera C (2010) Grammatical inference: learning automata and grammars. Cambridge University Press, New York, NY · Zbl 1227.68112 · doi:10.1017/CBO9781139194655
[28] Khalili A, Tacchella A (2014) Learning nondeterministic Mealy machines. In: Clark A, Kanazawa M, Yoshinaka R (eds) Proceedings of the 12th international conference on grammatical inference, ICGI 2014, Kyoto, Japan, September 17-19, 2014. JMLR workshop and conference proceedings, vol 34, pp 109-123. http://jmlr.org/proceedings/papers/v34/khalili14a.html
[29] Kwiatkowska, Marta; Norman, Gethin; Parker, David, PRISM 4.0: Verification of Probabilistic Real-Time Systems, 585-591 (2011), Berlin, Heidelberg · doi:10.1007/978-3-642-22110-1_47
[30] Kwiatkowska, Marta; Parker, David, Automated Verification and Strategy Synthesis for Probabilistic Systems, 5-22 (2013), Cham · Zbl 1410.68233 · doi:10.1007/978-3-319-02444-8_2
[31] Larsen, Kim G.; Legay, Axel, Statistical Model Checking: Past, Present, and Future, 3-15 (2016), Cham · doi:10.1007/978-3-319-47166-2_1
[32] Legay, Axel; Delahaye, Benoît; Bensalem, Saddek, Statistical Model Checking: An Overview, 122-135 (2010), Berlin, Heidelberg · doi:10.1007/978-3-642-16612-9_11
[33] Legay, Axel; Sedwards, Sean; Traonouez, Louis-Marie, Scalable Verification of Markov Decision Processes, 350-362 (2015), Cham · doi:10.1007/978-3-319-15201-1_23
[34] Mao H, Chen Y, Jaeger M, Nielsen TD, Larsen KG, Nielsen B (2011) Learning probabilistic automata for model checking. In: Eighth international conference on quantitative evaluation of systems, QEST 2011, Aachen, 5-8 September, 2011, pp 111-120. IEEE Computer Society. https://doi.org/10.1109/QEST.2011.21 · Zbl 1454.68061
[35] Mao, Hua; Chen, Yingke; Jaeger, Manfred; Nielsen, Thomas D.; Larsen, Kim G.; Nielsen, Brian, Learning Markov Decision Processes for Model Checking, Electronic Proceedings in Theoretical Computer Science, 103, 49-63 (2012) · doi:10.4204/EPTCS.103.6
[36] Mao, H.; Chen, Y.; Jaeger, M.; Nielsen, TD; Larsen, KG; Nielsen, B., Learning deterministic probabilistic automata from a model checking perspective, Mach Learn, 105, 255-299 (2016) · Zbl 1454.68061 · doi:10.1007/s10994-016-5565-9
[37] Margaria T, Niese O, Raffelt H, Steffen B (2004) Efficient test-based model generation for legacy reactive systems. In: Ninth IEEE international high-level design validation and test workshop 2004, Sonoma Valley, CA, USA, November 10-12, 2004, pp. 95-100. IEEE Computer Society. https://doi.org/10.1109/HLDVT.2004.1431246
[38] Nachmanson L, Veanes M, Schulte W, Tillmann N, Grieskamp W (2004) Optimal strategies for testing nondeterministic systems. In: Avrunin GS, Rothermel G (eds) Proceedings of the ACM/SIGSOFT international symposium on software testing and analysis, ISSTA 2004, Boston, MA, USA, July 11-14, 2004, pp 55-64. ACM. https://doi.org/10.1145/1007512.1007520
[39] Nouri, Ayoub; Raman, Balaji; Bozga, Marius; Legay, Axel; Bensalem, Saddek, Faster Statistical Model Checking by Means of Abstraction and Learning, 340-355 (2014), Cham · doi:10.1007/978-3-319-11164-3_28
[40] Okamoto, M., Some inequalities relating to the partial sum of binomial probabilities, Ann Inst Stat Math, 10, 29-35 (1959) · Zbl 0084.14001 · doi:10.1007/BF02883985
[41] Oncina J, Garcia P (1992) Identifying regular languages in polynomial time. In: Advances in structural and syntactic pattern recognition. Volume 5 of series in Machine perception and artificial intelligence, pp 99-108. World Scientific
[42] Peled DA, Vardi MY, Yannakakis M (1999) Black box checking. In: Wu J, Chanson ST, Gao Q (eds) Formal methods for protocol engineering and distributed systems, FORTE XII/PSTV XIX’99, IFIP TC6 WG6.1 joint international conference on formal description techniques for distributed systems and communication protocols (FORTE XII) and protocol specification, testing and verification (PSTV XIX), October 5-8, 1999, Beijing, China. IFIP conference proceedings, vol 156, pp 225-240. Kluwer · Zbl 0952.68012
[43] prob-black-reach—Java implementation of probabilistic black-box reachability checking. https://github.com/mtappler/prob-black-reach. Accessed 3 Dec 2018
[44] de Ruiter J, Poll E (2015) Protocol state fuzzing of TLS implementations. In: Jung J, Holz T(eds) 24th USENIX security symposium, USENIX Security 15, Washington, D.C., USA, August 12-14, 2015, pp 193-206. USENIX Association. https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/de-ruiter
[45] Sen, Koushik; Viswanathan, Mahesh; Agha, Gul, Statistical Model Checking of Black-Box Probabilistic Systems, 202-215 (2004), Berlin, Heidelberg · Zbl 1103.68639 · doi:10.1007/978-3-540-27813-9_16
[46] Shahbaz, Muzammil; Groz, Roland, Inferring Mealy Machines, 207-222 (2009), Berlin, Heidelberg · doi:10.1007/978-3-642-05089-3_14
[47] Shu G, Lee D (2007) 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. https://doi.org/10.1109/ICDCS.2007.147
[48] Sivakorn S, Argyros G, Pei K, Keromytis AD, Jana S (2017) HVLearn: automated black-box analysis of hostname verification in SSL/TLS implementations. In: SP 2017, pp 521-538. IEEE Computer Society. https://doi.org/10.1109/SP.2017.46
[49] Tappler M, Aichernig BK, Bloem R (2017) Model-based testing IoT communication via active automata learning. In: 2017 IEEE international conference on software testing, verification and validation, ICST 2017, Tokyo, Japan, March 13-17, 2017, pp 276-287. IEEE Computer Society. https://doi.org/10.1109/ICST.2017.32
[50] TCP models. https://gitlab.science.ru.nl/pfiteraubrostean/tcp-learner/tree/cav-aec/models. Accessed 3 Dec 2018
[51] Utting, M.; Pretschner, A.; Legeard, B., A taxonomy of model-based testing approaches, Softw Test Verif Reliab, 22, 297-312 (2012) · doi:10.1002/stvr.456
[52] Verwer, Sicco; de Weerdt, Mathijs; Witteveen, Cees, A Likelihood-Ratio Test for Identifying Probabilistic Deterministic Real-Time Automata from Positive Data, 203-216 (2010), Berlin, Heidelberg · Zbl 1291.68208 · doi:10.1007/978-3-642-15488-1_17
[53] Volpato M, Tretmans J (2015) Approximate active learning of nondeterministic input output transition systems. In: ECEASST, vol 72. http://journal.ub.tu-berlin.de/eceasst/article/view/1008
[54] Wang J, Sun J, Qin S Verifying complex systems probabilistically through learning, abstraction and refinement. In: CoRR. arXiv:1610.06371 (2016)
[55] Younes, Håkan L. S., Probabilistic Verification for “Black-Box” Systems, 253-265 (2005), Berlin, Heidelberg · Zbl 1081.68641 · doi:10.1007/11513988_25
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.