×

Improving active Mealy machine learning for protocol conformance testing. (English) Zbl 1317.68087

Summary: Using a well-known industrial case study from the verification literature, the bounded retransmission protocol, we show how active learning can be used to establish the correctness of protocol implementation \(I\) relative to a given reference implementation \(R\). Using active learning, we learn a model \(M_R\) of reference implementation \(R\), which serves as input for a model-based testing tool that checks conformance of implementation \(I\) to \(M_R\). In addition, we also explore an alternative approach in which we learn a model \(M_I\) of implementation \(I\), which is compared to model \(M_R\) using an equivalence checker. Our work uses a unique combination of software tools for model construction (Uppaal), active learning (LearnLib, Tomte), model-based testing (JTorX, TorXakis) and verification (CADP, MRMC). We show how these tools can be used for learning models of and revealing errors in implementations, present the new notion of a conformance oracle, and demonstrate how conformance oracles can be used to speed up conformance checking.

MSC:

68Q45 Formal languages and automata
68Q32 Computational learning theory
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aarts, F.; Vaandrager, F., Learning I/O automata, No. 6269, 71-85 (2010), Berlin · Zbl 1287.68087
[2] Aarts, F.; Jonsson, B.; Uijen, J., Generating models of infinite-state communication protocols using regular inference with abstraction, 188-204 (2010), Berlin
[3] Aarts, F.; Schmaltz, J.; Vaandrager, F., Inference and abstraction of the biometric passport, 673-686 (2010), Berlin · doi:10.1007/978-3-642-16558-0_54
[4] Aarts, F.; Heidarian, F.; Kuppens, H.; Olsen, P.; Vaandrager, F., Automata learning through counterexample-guided abstraction refinement, No. 7436, 10-27 (2012), Berlin · Zbl 1372.68153
[5] Aarts, F.; Kuppens, H.; Tretmans, J.; Vaandrager, F.; Verwer, S., Learning and testing the bounded retransmission protocol, No. 21, 4-18 (2012)
[6] Alur, R., & Dill, D. L. (1994). A theory of timed automata. Theoretical Computer Science, 126, 183-235. · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8
[7] Ammons, G.; Bodik, R.; Larus, J. R., Mining specifications, 4-16 (2002), New York · Zbl 1323.68361
[8] Angluin, D. (1987). Learning regular sets from queries and counterexamples. Information and Computation, 75(2), 87-106. · Zbl 0636.68112 · doi:10.1016/0890-5401(87)90052-6
[9] Antunes, J.; Neves, N.; Verissimo, P., Reverse engineering of protocols from network traces, 169-178 (2011)
[10] Aziz, A.; Sanwal, K.; Singhal, V.; Brayton, R., Verifying continuous time Markov chains, No. 1102, 269-276 (1996), Berlin
[11] Balcázar, J., Dıaz, J., Gavaldá, R., & Watanabe, O. (1997). Algorithms for learning finite automata from queries: a unified view. Advances in Algorithms, Languages, and Complexity, 53-72. · Zbl 0874.68260
[12] Bartlett, K., Scantlebury, R., & Wilkinson, P. (1969). A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM, 12, 260-261. · doi:10.1145/362946.362970
[13] Behrmann, G.; David, A.; Larsen, K., A tutorial on Uppaal, No. 3185, 33-35 (2004), Berlin · Zbl 1105.68350 · doi:10.1007/978-3-540-30080-9_7
[14] Belinfante, A., Jtorx: a tool for on-line model-driven test derivation and execution, No. 6015, 266-270 (2010), Berlin · doi:10.1007/978-3-642-12002-2_21
[15] Berg, T.; Grinchtein, O.; Jonsson, B.; Leucker, M.; Raffelt, H.; Steffen, B., On the correspondence between conformance testing and regular inference, No. 3442, 175-189 (2005), Berlin · Zbl 1119.68366 · doi:10.1007/978-3-540-31984-9_14
[16] Bertolino, A.; Inverardi, P.; Pelliccione, P.; Tivoli, M., Automatic synthesis of behavior protocols for composable web-services, 141-150 (2009), New York
[17] Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., & Pretschner, A. (Eds.) (2005). Lecture notes in computer science.: Vol.3472. Model-based testing of reactive systems. Berlin: Springer. · Zbl 1070.68088
[18] Castro, J.; Gavaldà, R., Towards feasible PAC-learning of probabilistic deterministic finite automata, No. 5278, 163-174 (2008), Berlin · Zbl 1177.68108 · doi:10.1007/978-3-540-88009-7_13
[19] Cho, C. Y.; Babic, D.; Shin, E. C. R.; Song, D., Inference and analysis of formal models of botnet command and control protocols, 426-439 (2010), New York · doi:10.1145/1866307.1866355
[20] Clark, A., & Thollard, F. (2004). PAC-learnability of probabilistic deterministic finite state automata. Journal of Machine Learning Research, 473-497. · Zbl 1222.68094
[21] Clarke, E., Model checking, No. 1346, 54-56 (1997), Berlin · doi:10.1007/BFb0058022
[22] Combe, D.; Higuera, C.; Janodet, J.-C., Zulu: an interactive learning competition, No. 6062, 139-146 (2010), Berlin · doi:10.1007/978-3-642-14684-8_15
[23] Comparetti, P.; Wondracek, G.; Kruegel, C.; Kirda, E., Prospex: protocol specification extraction, 110-125 (2009), New York
[24] Cook, J. E., & Wolf, A. L. (1998). Discovering models of software processes from event-based data. ACM Transactions on Software Engineering and Methodology, 7, 215-249. · doi:10.1145/287000.287001
[25] Cui, W.; Kannan, J.; Wang, H. J., Discoverer: automatic protocol reverse engineering from network traces, 14 (2007)
[26] Dalal, S.; Jain, A.; Karunanithi, N.; Leaton, J.; Lott, C.; Patton, G.; Horowitz, B., Model-based testing in practice, 285-294 (1999), New York
[27] Dallmeier, V.; Lindig, C.; Wasylkowski, A.; Zeller, A., Mining object behavior with ADABU, 17-24 (2006), New York · doi:10.1145/1138912.1138918
[28] D’Argenio, P.; Katoen, J.-P.; Ruys, T.; Tretmans, J., The bounded retransmission protocol must be on time!, No. 1217, 416-431 (1997), Berlin · doi:10.1007/BFb0035403
[29] de la Higuera, C. (2010). Grammatical inference: learning automata and grammars. New York: Cambridge University Press. · Zbl 1227.68112
[30] de la Higuera, C., & Janodet, J.-C. (2004). Inference of omega-languages from prefixes. Theoretical Computer Science, 313(2), 295-312. · Zbl 1069.68071 · doi:10.1016/j.tcs.2003.11.009
[31] Denis, F.; Lemay, A.; Terlutte, A., Learning regular languages using non deterministic finite automata, 39-50 (2000) · Zbl 0974.68088
[32] Dijkstra, E. (1969). Notes on structured programming.
[33] Frantzen, L.; Tretmans, J.; Willemse, T., Test generation based on symbolic specifications, No. 3395, 1-15 (2005), Berlin · Zbl 1081.68570 · doi:10.1007/978-3-540-31848-4_1
[34] Garavel, H.; Lang, F.; Mateescu, R.; Serwe, W., CADP 2010: a toolbox for the construction and analysis of distributed processes, No. 6605, 372-387 (2011), Berlin · Zbl 1316.68074 · doi:10.1007/978-3-642-19835-9_33
[35] Gold, E. M. (1978). Complexity of automaton identification from given data. Information and Control, 37(3), 302-320. · Zbl 0376.68041 · doi:10.1016/S0019-9958(78)90562-4
[36] Grinchtein, O.; Jonsson, B.; Petterson, P., Inference of event-recording automata using timed decision trees, No. 4137, 435-449 (2006), Berlin · Zbl 1151.68459
[37] Hansson, H., & Jonsson, B. (1994). A logic for reasoning about time and reliability. Formal Aspects of Computing, 6, 512-535. · Zbl 0820.68113 · doi:10.1007/BF01211866
[38] Helmink, L.; Sellink, M.; Vaandrager, F., Proof-checking a data link protocol, No. 806, 127-165 (1994), Berlin
[39] Henzinger, T., Nicollin, X., Sifakis, J., & Yovine, S. (1994). Symbolic model checking for real-time systems. Information and Computation, 111(2), 193-244. · Zbl 0806.68080 · doi:10.1006/inco.1994.1045
[40] Hungar, H.; Niese, O.; Steffen, B., Domain-specific optimization in automata learning, No. 2725, 315-327 (2003), Berlin · Zbl 1278.68177 · doi:10.1007/978-3-540-45069-6_31
[41] Ip, C., & Dill, D. (1996). Better verification through symmetry. Formal Methods in System Design, 9(1/2), 41-75.
[42] Katoen, J.-P., Zapreev, I. S., Hahn, E. M., Hermanns, H., & Jansen, D. N. (2011). The ins and outs of the probabilistic model checker MRMC. Performance Evaluation, 68(2), 90-104. · doi:10.1016/j.peva.2010.04.001
[43] Kearns, M. J., & Vazirani, U. V. (1994). An introduction to computational learning theory. Cambridge: MIT Press.
[44] Lee, D., & Yannakakis, M. (1996). Principles and methods for testing finite state machines—a survey. Proceedings of the IEEE, 84(8), 1090-1123. · doi:10.1109/5.533956
[45] Margaria, T.; Niese, O.; Raffelt, H.; Steffen, B., Efficient test-based model generation for legacy reactive systems, 95-100 (2004), Washington
[46] Mariani, L., Pastore, F., & Pezze, M. (2011). Dynamic analysis for diagnosing integration faults. IEEE Transactions on Software Engineering, 37, 486-508. · doi:10.1109/TSE.2010.93
[47] Meinke, K.; Walkinshaw, N., Model-based testing and model inference, No. 7609, 440-443 (2012), Berlin
[48] Mostowski, W.; Poll, E.; Schmaltz, J.; Tretmans, J.; Wichers Schreur, R., Model-based testing of electronic passports, No. 5825, 207-209 (2009), Berlin · doi:10.1007/978-3-642-04570-7_19
[49] Puterman, M. L. (1994). Markov decision processes: discrete stochastic dynamic programming (1st ed.). New York: Wiley. · Zbl 0829.90134 · doi:10.1002/9780470316887
[50] Raffelt, H., Steffen, B., Berg, T., & Margaria, T. (2009). Learnlib: a framework for extrapolating behavioral models. International Journal on Software Tools for Technology Transfer, 11, 393-407. · doi:10.1007/s10009-009-0111-8
[51] Settles, B. (2010). Active learning literature survey (Technical report). University of Wisconsin-Madison.
[52] Shafique, M., & Labiche, Y. (2010). A systematic review of model based testing tool support (Technical Report SCE-10-04). Department of Systems and Computer Engineering, Carleton University, Ottawa, Canada.
[53] Sudkamp, T. A. (2006). Languages and machines: an introduction to the theory of computer science (3rd ed.). Reading: Addison-Wesley.
[54] Tretmans, J., Model based testing with labelled transition systems, No. 4949, 1-38 (2008), Berlin · doi:10.1007/978-3-540-78917-8_1
[55] Tretmans, J.; Brinksma, E., Torx: automated model-based testing, 31-43 (2003)
[56] Utting, M., & Legeard, B. (2007). Practical model-based testing: a tools approach. San Mateo: Morgan-Kaufmann.
[57] van der Aalst, W. M. P. (2011). Process mining—discovery, conformance and enhancement of business processes. Berlin: Springer. · Zbl 1216.68016
[58] Verwer, S. (2010). Efficient identification of timed automata: theory and practice. PhD thesis, Delft University of Technology.
[59] Verwer, S., de Weerdt, M., & Witteveen, C. (2011). Efficiently identifying deterministic real-time automata from labeled data. Machine Learning, 1-39. · Zbl 1238.68135
[60] Walkinshaw, N.; Bogdanov, K.; Holcombe, M.; Salahuddin, S., Reverse engineering state machines by interactive grammar inference, 209-218 (2007), New York
[61] Walkinshaw, N.; Bogdanov, K.; Damas, C.; Lambeau, B.; Dupont, P., A framework for the competitive evaluation of model inference techniques, 1-9 (2010), New York
[62] Walkinshaw, N.; Bogdanov, K.; Derrick, J.; Paris, J., Increasing functional coverage by inductive testing: a case study, No. 6435, 126-141 (2010), Berlin
[63] Weyuker, E. J. (1983). Assessing test data adequacy through program inference. ACM Transactions on Programming Languages and Systems, 5(4), 641-655. · Zbl 0517.68031 · doi:10.1145/69575.357231
[64] Yokomori, T. (1993). Learning non-deterministic finite automata from queries and counterexamples. In Machine Intelligence (pp. 196-189). University Press.
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.