Probabilistic black-box reachability checking (extended version)

Aichernig BK, Mostowski W, Mousavi MR, Tappler M, Taromirad M (2018) Model learning and model-based testing. In: Bennaceur A, Hähnle R, Meinke K (eds) Machine learning for dynamic software analysis: potentials and limits–international Dagstuhl seminar 16172, Dagstuhl Castle, Germany, April 24–27, 2016. Revised papers, Lecture notes in computer science, vol 11026, pp 74–100. Springer. https://doi.org/10.1007/978-3-319-96562-8_3 Aichernig BK, Tappler M (2017) Learning from faults: mutation testing in active automata learning. In: Barrett C, Davies M, Kahsai T (eds) NASA formal methods–9th international symposium, NFM 2017, Moffett Field, CA, USA, May 16–18, 2017. Proceedings, Lecture notes in computer science, vol 10227, pp 19–34. https://doi.org/10.1007/978-3-319-57288-8_2 Aichernig BK, Tappler M (2017) Probabilistic black-box reachability checking. In: Lahiri SK, Reger G (eds) Runtime verification–17th international conference, RV 2017, Seattle, WA, USA, September 13–16, 2017. Proceedings, Lecture notes in computer science, vol 10548, pp 50–67. Springer. https://doi.org/10.1007/978-3-319-67531-2_4 Angluin D (1987) Learning regular sets from queries and counterexamples. Inf. Comput. 75(2):87–106. https://doi.org/10.1016/0890-5401(87)90052-6 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 Aspnes J, Herlihy M (1990) Fast randomized consensus using shared memory. J Algorithms 11(3):441–461. https://doi.org/10.1016/0196-6774(90)90021-6 Baier C, Katoen J (2008) Principles of model checking. MIT Press, Cambridge 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 Beimel A, Bergadano F, Bshouty NH, Kushilevitz E, Varricchio S (2000) Learning functions represented as multiplicity automata. J ACM 47(3):506–530. https://doi.org/10.1145/337244.337257 Brázdil T, Chatterjee K, Chmelik M, Forejt V, Kretínský J, Kwiatkowska MZ, Parker D, Ujma M Verification of Markov decision processes using learning algorithms. In: Cassez and Raskin [12], pp 98–114. https://doi.org/10.1007/978-3-319-11936-6_8 Carrasco RC, Oncina J(1994) Learning stochastic regular grammars by means of a state merging method. In: Carrasco RC, Oncina J (eds) Grammatical inference and applications, second international colloquium, ICGI-94, Alicante, Spain, September 21–23, 1994. Proceedings, Lecture notes in computer science, vol 862, pp 139–152. Springer. https://doi.org/10.1007/3-540-58473-0_144 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 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 D’Argenio P, Legay A, Sedwards S, Traonouez L (2015) Smart sampling for lightweight verification of Markov decision processes. STTT 17(4):469–484. https://doi.org/10.1007/s10009-015-0383-0 David A, Jensen PG, Larsen KG, Legay A, Lime D, Sørensen MG, Taankvist JH. On time with minimal expected cost! In: Cassez and Raskin [12], pp 129–145. https://doi.org/10.1007/978-3-319-11936-6_10 David A, Jensen PG, Larsen KG, Mikucionis M, Taankvist JH (2015) Uppaal stratego. In: Baier C, Tinelli C (eds) Tools and algorithms for the construction and analysis of systems–21st international conference, TACAS 2015, held as part of the European joint conferences on theory and practice of software, ETAPS 2015, London, April 11–18, 2015. Proceedings, Lecture notes in computer science, vol 9035, pp 206–211. Springer. https://doi.org/10.1007/978-3-662-46681-0_16 Elkind E, Genest B, Peled DA, Qu H (2006) Grey-box checking. In: Najm E, Pradat-Peyre J, Donzeau-Gouge V (eds) Formal techniques for networked and distributed systems–FORTE 2006, 26th IFIP WG 6.1 international conference, Paris, France, September 26–29, 2006. Lecture notes in computer science, vol 4229, pp 420–435. Springer. https://doi.org/10.1007/11888116_30 EMQ. http://emqtt.io/. Accessed 3 Dec 2018 Feng L, Han T, Kwiatkowska MZ, Parker D (2011) Learning-based compositional verification for synchronous probabilistic systems. In: Bultan T, Hsiung P (eds) Automated technology for verification and analysis, 9th international symposium, ATVA 2011, Taipei, Taiwan, October 11–14, 2011. Proceedings, Lecture notes in computer science, vol 6996, pp 511–521. Springer. https://doi.org/10.1007/978-3-642-24372-1_40 Fiterau-Brostean P, Janssen R, Vaandrager FW (2016) Combining model learning and model checking to analyze TCP implementations. In: Chaudhuri S, Farzan A (eds) Computer aided verification–28th international conference, CAV 2016, Toronto, ON, Canada, July 17–23, 2016. Proceedings, Part II, Lecture notes in computer science, vol 9780, pp 454–471. Springer. https://doi.org/10.1007/978-3-319-41540-6_25 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 Forejt V, Kwiatkowska MZ, Norman G, Parker D (2011) Automated verification techniques for probabilistic systems. In: Bernardo M, Issarny V (eds) Formal methods for eternal networked software systems–11th international school on formal methods for the design of computer, communication and software systems, SFM 2011, Bertinoro, Italy, June 13–18, 2011. Advanced lectures, Lecture notes in computer science, vol 6659, pp 53–113. Springer. https://doi.org/10.1007/978-3-642-21455-4_3 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 Giantamidis G, Tripakis S (2016) Learning Moore machines from input-output traces. In: Fitzgerald JS, Heitmeyer CL, Gnesi S, Philippou A (eds) FM 2016: formal methods–21st international symposium, Limassol, Cyprus, November 9–11, 2016. Proceedings, Lecture notes in computer science, vol 9995, pp 291–309. https://doi.org/10.1007/978-3-319-48989-6_18 Grinchtein O, Jonsson B, Leucker M (2004) Learning of event-recording automata. In: Lakhnech Y, Yovine S (eds) Formal techniques, modelling and analysis of timed and fault-tolerant systems, joint international conferences on formal modelling and analysis of timed systems, FORMATS 2004 and formal techniques in real-time and fault-tolerant systems, FTRTFT 2004, Grenoble, France, September 22–24, 2004. Proceedings, Lecture notes in computer science, vol 3253, pp 379–396. Springer. https://doi.org/10.1007/978-3-540-30206-3_26 Groce A, Peled DA, Yannakakis M (2002) Adaptive model checking. In: Katoen J, Stevens P (eds) Tools and algorithms for the construction and analysis of systems. In: 8th international conference, TACAS 2002, held as part of the joint European conference on theory and practice of software, ETAPS 2002, Grenoble, France, April 8–12, 2002. Proceedings, Lecture notes in computer science de la Higuera C (2010) Grammatical inference: learning automata and grammars. Cambridge University Press, New York, NY 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 Kwiatkowska MZ, Norman G, Parker D (2011) PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan G, Qadeer S (eds) Computer aided verification–23rd international conference, CAV 2011, Snowbird, UT, July 14–20, 2011. Proceedings, Lecture notes in computer science, vol 6806, pp 585–591. Springer. https://doi.org/10.1007/978-3-642-22110-1_47 Kwiatkowska MZ, Parker D (2013) Automated verification and strategy synthesis for probabilistic systems. In: Hung DV, Ogawa M (eds) Automated technology for verification and analysis–11th international symposium, ATVA 2013, Hanoi, Vietnam, October 15–18, 2013. Proceedings, Lecture notes in computer science, vol 8172, pp 5–22. Springer. https://doi.org/10.1007/978-3-319-02444-8_2 Larsen KG, Legay A (2016) Statistical model checking: past, present, and future. In: Margaria T, Steffen B (eds) Leveraging applications of formal methods, verification and validation: foundational techniques–7th international symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10–14, 2016. Proceedings, Part I, Lecture notes in computer science, vol 9952, pp 3–15. https://doi.org/10.1007/978-3-319-47166-2_1 Legay A, Delahaye B, Bensalem S (2010) Statistical model checking: an overview. In: Barringer H, Falcone Y, Finkbeiner B, Havelund K, Lee I, Pace GJ, Rosu G, Sokolsky O, Tillmann N (eds) Runtime verification–first international conference, RV 2010, St. Julians, Malta, November 1–4, 2010. Proceedings, Lecture notes in computer science, vol 6418, pp 122–135. Springer. https://doi.org/10.1007/978-3-642-16612-9_11 Legay A, Sedwards S, Traonouez L (2014) Scalable verification of Markov decision processes. In: Canal C, Idani A (eds) Software engineering and formal methods–SEFM 2014 collocated workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS, Grenoble, France, September 1–2, 2014. Revised selected papers, Lecture notes in computer science, vol 8938, pp 350–362. Springer. https://doi.org/10.1007/978-3-319-15201-1_23 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 Mao H, Chen Y, Jaeger M, Nielsen TD, Larsen KG, Nielsen B (2012) Learning Markov decision processes for model checking. In: Fahrenberg U, Legay A, Thrane CR (eds) Proceedings quantities in formal methods, QFM 2012, Paris, France, 28 August 2012. EPTCS, vol 103, pp 49–63. https://doi.org/10.4204/EPTCS.103.6 Mao H, Chen Y, Jaeger M, Nielsen TD, Larsen KG, Nielsen B (2016) Learning deterministic probabilistic automata from a model checking perspective. Mach Learn 105(2):255–299. https://doi.org/10.1007/s10994-016-5565-9 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 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 Nouri A, Raman B, Bozga M, Legay A, Bensalem S (2014) Faster statistical model checking by means of abstraction and learning. In: Bonakdarpour B, Smolka SA (eds) Runtime verification–5th international conference, RV 2014, Toronto, ON, Canada, September 22–25, 2014. Proceedings, Lecture notes in computer science, vol 8734, pp 340–355. Springer. https://doi.org/10.1007/978-3-319-11164-3_28 Okamoto M (1959) Some inequalities relating to the partial sum of binomial probabilities. Ann Inst Stat Math 10(1):29–35. https://doi.org/10.1007/BF02883985 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 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 prob-black-reach—Java implementation of probabilistic black-box reachability checking. https://github.com/mtappler/prob-black-reach. Accessed 3 Dec 2018 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 Sen K, Viswanathan M, Agha G (2004) Statistical model checking of black-box probabilistic systems. In: Alur R, Peled DA (eds) Computer aided verification, 16th international conference, CAV 2004, Boston, MA, USA, July 13–17, 2004. Proceedings, Lecture notes in computer science, vol 3114, pp 202–215. Springer. https://doi.org/10.1007/978-3-540-27813-9_16 Shahbaz M, Groz R (2009) Inferring Mealy machines. In: Cavalcanti A, Dams D (eds) FM 2009: formal methods, second world congress, Eindhoven, The Netherlands, November 2–6, 2009. Proceedings, Lecture notes in computer science, vol 5850, pp 207–222. Springer. https://doi.org/10.1007/978-3-642-05089-3_14 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 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 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 TCP models. https://gitlab.science.ru.nl/pfiteraubrostean/tcp-learner/tree/cav-aec/models. Accessed 3 Dec 2018 Utting M, Pretschner A, Legeard B (2012) A taxonomy of model-based testing approaches. Softw Test Verif Reliab 22(5):297–312. https://doi.org/10.1002/stvr.456 Verwer S, de Weerdt M, Witteveen C (2010) A likelihood-ratio test for identifying probabilistic deterministic real-time automata from positive data. In: Sempere JM, García P (eds) Grammatical inference: theoretical results and applications, 10th international colloquium, ICGI 2010, Valencia, Spain, September 13–16, 2010. Proceedings, Lecture notes in computer science, vol 6339, pp 203–216. Springer. https://doi.org/10.1007/978-3-642-15488-1_17 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 Wang J, Sun J, Qin S Verifying complex systems probabilistically through learning, abstraction and refinement. In: CoRR. arXiv:1610.06371 (2016) Younes HLS (2005) Probabilistic verification for “black-box” systems. In: Etessami K, Rajamani SK (eds) Computer aided verification, 17th international conference, CAV 2005, Edinburgh, Scotland, July 6–10, 2005. Proceedings, Lecture notes in computer science, vol 3576, pp 253–265. Springer. https://doi.org/10.1007/11513988_25