Abstract
We describe a large collection of benchmarks, publicly available through the wiki automata.cs.ru.nl, of different types of state machine models: DFAs, Moore machines, Mealy machines, interface automata and register automata. Our repository includes both randomly generated state machines and models of real protocols and embedded software/hardware systems. These benchmarks will allow researchers to evaluate the performance of new algorithms and tools for active automata learning and conformance testing.
R. Smetsers—Supported by NWO/EW project 628.001.009 (LEMMA).
F. Vaandrager—Supported by NWO project 13859 (SUMBAT).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Following Hopcroft and Ullman [32], we ignore the initial output in order to obtain equivalence of Moore and Mealy machines.
- 2.
If \(\varGamma = \emptyset \) then also \(\rightarrow = \emptyset \), which means that \(\mathcal{M}\) is equivalent to \(\mathcal{M}\) with \(\varGamma \) replaced by an arbitrary set. Thus, we may assume w.l.o.g. that \(\varGamma \ne \emptyset \).
- 3.
- 4.
Actually, our repository supports actions with zero or more data parameters, but this assumption simplifies the presentation.
References
Aarts, F., Fiterau-Brostean, P., Kuppens, H., Vaandrager, F.: Learning register automata with fresh value generation. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 165–183. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25150-9_11
Aarts, F., Heidarian, F., Kuppens, H., Olsen, P., Vaandrager, F.: Automata learning through counterexample guided abstraction refinement. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 10–27. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32759-9_4
Aarts, F., Howar, F., Kuppens, H., Vaandrager, F.: Algorithms for inferring register automata. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8802, pp. 202–219. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45234-9_15
Aarts, F., Jonsson, B., Uijen, J.: Generating models of infinite-state communication protocols using regular inference with abstraction. In: Petrenko, A., Simão, A., Maldonado, J.C. (eds.) ICTSS 2010. LNCS, vol. 6435, pp. 188–204. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16573-3_14
Aarts, F., Kuppens, H., Tretmans, G.J., Vaandrager, F.W., Verwer, S.: Improving active Mealy machine learning for protocol conformance testing. Mach. Learn. 96(1–2), 189–224 (2014)
Aarts, F., de Ruiter, J., Poll, E.: Formal models of bank cards for free. In: IEEE International Conference on Software Testing Verification and Validation Workshop, Los Alamitos, CA, USA, pp. 461–468. IEEE Computer Society (2013)
Aarts, F., Schmaltz, J., Vaandrager, F.: Inference and abstraction of the biometric passport. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010. LNCS, vol. 6415, pp. 673–686. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16558-0_54
Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)
Berg, T., Grinchtein, O., Jonsson, B., Leucker, M., Raffelt, H., Steffen, B.: On the correspondence between conformance testing and regular inference. In: Cerioli, M. (ed.) FASE 2005. LNCS, vol. 3442, pp. 175–189. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31984-9_14
Bollig, B., Habermehl, P., Kern, C., Leucker, M.: Angluin-style learning of NFA. In: Boutilier, C. (ed.) Proceedings of IJCAI 2009, pp. 1004–1009 (2009)
Bollig, B., Katoen, J.-P., Kern, C., Leucker, M., Neider, D., Piegdon, D.R.: libalf: The automata learning framework. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 360–364. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_32
Brglez, F.: ACM/SIGDA benchmark dataset (1996). http://people.engr.ncsu.edu/brglez/CBL/benchmarks/Benchmarks-upto-1996.html. Accessed 14 Aug 2018
BSI: Advanced security mechanisms for machine readable travel documents - extended access control (EAC) - version 1.11. Technical report TR-03110, German Federal Office for Information Security (BSI), Bonn, Germany (2008)
Cassel, S., Howar, F., Jonsson, B., Merten, M., Steffen, B.: A succinct canonical register automaton model. J. Log. Algebr. Meth. Program. 84(1), 54–66 (2015)
Cassel, S., Howar, F., Jonsson, B., Steffen, B.: Active learning for extended finite state machines. Formal Asp. Comput. 28(2), 233–263 (2016)
Chalupar, G., Peherstorfer, S., Poll, E., de Ruiter, J.: Automated reverse engineering using Lego. In: Proceedings WOOT 2014, Los Alamitos, CA, USA. IEEE Computer Society, August 2014
Champarnaud, J.-M., Paranthoën, T.: Random generation of DFAs. Theor. Comput. Sci. 330(2), 221–235 (2005)
van Dalen, D.: Logic and Structure. Springer, London (1983)
D’Antoni, L.: AutomatArk. https://github.com/lorisdanto/automatark. Accessed 14 Aug 2018
D’Argenio, P.R., Katoen, J.-P., Ruys, T.C., Tretmans, J.: The bounded retransmission protocol must be on time!. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 416–431. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0035403
de Alfaro, L., Henzinger, T.A.: Interface automata. In: Proceedings ESEC/FSE-01, Software Engineering Notes, vol. 26, pp. 109–120. ACM Press, New York, September 2001
Heidarian Dehkordi, F.: Studies on verification of wireless sensor networks and abstraction learning for system inference. Ph.D. thesis, Radboud University Nijmegen, July 2012
Dorofeeva, R., El-Fakih, K., Maag, S., Cavalli, A.R., Yevtushenko, N.: FSM-based conformance testing methods: a survey annotated with experimental evaluation. Inf. Softw. Technol. 52(12), 1286–1297 (2010)
Fiser, P.: Collection of digital design benchmarks. https://ddd.fit.cvut.cz/prj/Benchmarks/. Accessed 14 Aug 2018
Fiterău-Broştean, P., Howar, F.: Learning-based testing the sliding window behavior of TCP implementations. In: Petrucci, L., Seceleanu, C., Cavalcanti, A. (eds.) FMICS/AVoCS -2017. LNCS, vol. 10471, pp. 185–200. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-67113-0_12
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). https://doi.org/10.1007/978-3-319-41540-6_25
Fiterău-Broştean, P., Lenaerts, T., Poll, E., de Ruiter, J., Vaandrager, F., Verleg, P.: Model learning and model checking of SSH implementations. In: Proceedings SPIN Symposium, SPIN 2017, pp. 142–151. ACM, New York (2017)
Gansner, E.R., North, S.C.: An open graph visualization system and its applications to software engineering. Softw. Pract. Exper. 30(11), 1203–1233 (2000)
Harary, F., Palmer, E.M.: Enumeration of finite automata. Inf. Control. 10(5), 499–508 (1967)
Helmink, L., Sellink, M.P.A., Vaandrager, F.W.: Proof-checking a data link protocol. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 127–165. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58085-9_75
Hierons, R.M., Türker, U.C.: Incomplete distinguishing sequences for finite state machines. Comput. J. 58(11), 3089–3113 (2015)
Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Boston (1979)
Howar, F.: Active learning of interface programs. Ph.D. thesis, University of Dortmund, June 2012
Howar, F., Isberner, M., Steffen, B., Bauer, O., Jonsson, B.: Inferring semantic interfaces of data structures. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 554–571. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34026-0_41
Howar, F., Steffen, B.: Active automata learning in practice. In: Bennaceur, A., Hähnle, R., Meinke, K. (eds.) Machine Learning for Dynamic Software Analysis: Potentials and Limits. LNCS, vol. 11026, pp. 123–148. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96562-8_5
ICAO: Doc 9303 - machine readable travel documents - part 1–2. Technical report, International Civil Aviation Organization, Sixth edition (2006)
Isberner, M., Howar, F., Steffen, B.: The TTT algorithm: a redundancy-free approach to active automata learning. In: Bonakdarpour, B., Smolka, S.A. (eds.) RV 2014. LNCS, vol. 8734, pp. 307–322. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-11164-3_26
Jasper, M., et al.: The RERS 2017 challenge and workshop (invited paper). In: Proceedings SPIN Symposium, pp. 11–20. ACM (2017)
Jonsson, B.: Modular verification of asynchronous networks. In: PODC 1987 [54], pp. 152–166
Kearns, M.J., Vazirani, U.V.: An Introduction to Computational Learning Theory. MIT Press, Cambridge (1994)
Keller, R.M.: Formal verification of parallel programs. Commun. ACM 19(7), 371–384 (1976)
Lang, K.J., Pearlmutter, B.A., Price, R.A.: Results of the Abbadingo one DFA learning competition and a new evidence-driven state merging algorithm. In: Honavar, V., Slutzki, G. (eds.) ICGI 1998. LNCS, vol. 1433, pp. 1–12. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0054059
Lee, D., Yannakakis, M.: Testing finite-state machines: state identification and verification. IEEE Trans. Comput. 43(3), 306–320 (1994)
Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines — a survey. Proc. IEEE 84(8), 1090–1123 (1996)
Leskovec, J., Kleinberg, J.M., Faloutsos, C.: Graph evolution: densification and shrinking diameters. TKDD 1(1), 1–41 (2007). https://doi.org/10.1145/1217299.1217301
Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Fransisco (1996)
Lynch, N.A., Tuttle, M.R.: Hierarchical correctness proofs for distributed algorithms. In: PODC 1987 [54], pp. 137–151. A full version is available as MIT Technical Report MIT/LCS/TR-387
Mealy, G.H.: A method for synthesizing sequential circuits. Bell Syst. Tech. J. 34(5), 1045–1079 (1955)
Merten, M., Steffen, B., Howar, F., Margaria, T.: Next generation LearnLib. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 220–223. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19835-9_18
Moerman, J., Sammartino, M., Silva, A., Klin, B., Szynwelski, M.: Learning nominal automata. In: Proceedings POPL 2017, pp. 613–625. ACM (2017)
Moore, E.F.: Gedanken-experiments on sequential machines. In: Automata Studies. Annals of Mathematics Studies, vol. 34, pp. 129–153. Princeton University Press (1956)
Naik, K.: Efficient computation of unique input/output sequences in finite-state machines. IEEE/ACM Trans. Netw. 5(4), 585–599 (1997)
Nicaud, C.: Étude du comportement en moyenne des automates finis et des langages rationnels. Ph.D. thesis, Université Paris 7 (2000)
Proceedings of the 6th Annual ACM Symposium on Principles of Distributed Computing, August 1987
Raffelt, H., Steffen, B., Berg, T.: LearnLib: a library for automata learning and experimentation. In: Proceedings FMICS 2005, pp. 62–71. ACM Press, New York (2005)
Raffelt, H., Steffen, B., Berg, T., Margaria, T.: LearnLib: a framework for extrapolating behavioral models. STTT 11(5), 393–407 (2009)
Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Inf. Comput. 103(2), 299–347 (1993)
de Ruiter, J., Poll, E.: Protocol state fuzzing of TLS implementations. In: Proceedings USENIX Security 15, pp. 193–206. USENIX Association, August 2015
Schuts, M.: Industrial experiences in applying domain specific languages for system evolution. Ph.D. thesis, Radboud University Nijmegen, September 2017
Schuts, M., Hooman, J., Vaandrager, F.: Refactoring of legacy software using model learning and equivalence checking: an industrial experience report. In: Ábrahám, E., Huisman, M. (eds.) IFM 2016. LNCS, vol. 9681, pp. 311–325. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33693-0_20
Shahbaz, M., Groz, R.: Inferring Mealy machines. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 207–222. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-05089-3_14
Smeenk, W., Moerman, J., Vaandrager, F., Jansen, D.N.: Applying automata learning to embedded control software. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 67–83. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25423-4_5
Steffen, B., Howar, F., Merten, M.: Introduction to active automata learning from a practical perspective. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 256–296. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21455-4_8
Tappler, M., Aichernig, B.K., Bloem, R.: Model-based testing IoT communication via active automata learning. In: Proceedings ICST 2017, pp. 276–287. IEEE Computer Society (2017)
Tretmans, J.: Test generation with inputs, outputs, and repetitive quiescence. Softw. Concepts Tools 17, 103–120 (1996)
Tretmans, J.: Model based testing with labelled transition systems. In: Hierons, R.M., Bowen, J.P., Harman, M. (eds.) Formal Methods and Testing. LNCS, vol. 4949, pp. 1–38. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78917-8_1
Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing approaches. Softw. Test. Verif. Reliab. 22(5), 297–312 (2012)
Vaandrager, F.W.: Model learning. Commun. ACM 60(2), 86–95 (2017)
Volpato, M., Tretmans, J.: Towards quality of model-based testing in the ioco framework. In: Proceedings JAMAICA 2013, pp. 41–46. ACM, New York (2013)
Walkinshaw, N., Bogdanov, K., Damas, C., Lambeau, B., Dupont, P.: A framework for the competitive evaluation of model inference techniques. In: Proceedings MIIT 2010, pp. 1–9. ACM (2010)
Walkinshaw, N., Lambeau, B., Damas, C., Bogdanov, K., Dupont, P.: STAMINA: a competition to encourage the development and assessment of software model inference techniques. Empir. Softw. Eng. 18(4), 791–824 (2013)
Acknowledgements
This article was initiated at the Dagstuhl Seminar 16172 “Machine Learning for Dynamic Software Analysis: Potentials and Limits” organized by Amel Bennaceur, Reiner Hähnle, and Karl Meinke. We thank Fides Aarts, Petra van den Bos, Alexander Fedotov, Paul Fiterău-Broştean, Falk Howar, Joshua Moerman, Erik Poll, and Joeri de Ruiter for helping with the repository. Many thanks to Pierre van de Laar and the anonymous reviewers for their suggestions on an earlier version of this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Neider, D., Smetsers, R., Vaandrager, F., Kuppens, H. (2019). Benchmarks for Automata Learning and Conformance Testing. In: Margaria, T., Graf, S., Larsen, K. (eds) Models, Mindsets, Meta: The What, the How, and the Why Not?. Lecture Notes in Computer Science(), vol 11200. Springer, Cham. https://doi.org/10.1007/978-3-030-22348-9_23
Download citation
DOI: https://doi.org/10.1007/978-3-030-22348-9_23
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-22347-2
Online ISBN: 978-3-030-22348-9
eBook Packages: Computer ScienceComputer Science (R0)