×

zbMATH — the first resource for mathematics

Inferring canonical register automata. (English) Zbl 1326.68168
Kuncak, Viktor (ed.) et al., Verification, model checking, and abstract interpretation. 13th international conference, VMCAI 2012, Philadelphia, PA, USA, January 22–24, 2012. Proceedings. Berlin: Springer (ISBN 978-3-642-27939-3/pbk). Lecture Notes in Computer Science 7148, 251-266 (2012).
Summary: In this paper, we present an extension of active automata learning to register automata, an automaton model which is capable of expressing the influence of data on control flow. Register automata operate on an infinite data domain, whose values can be assigned to registers and compared for equality. Our active learning algorithm is unique in that it directly infers the effect of data values on control flow as part of the learning process. This effect is expressed by means of registers and guarded transitions in the resulting register automata models. The application of our algorithm to a small example indicates the impact of learning register automata models: Not only are the inferred models much more expressive than finite state machines, but the prototype implementation also drastically outperforms the classic \(L ^{*}\) algorithm, even when exploiting optimal data abstraction and symmetry reduction.
For the entire collection see [Zbl 1236.68007].

MSC:
68Q32 Computational learning theory
68Q45 Formal languages and automata
Software:
Daikon; XMPP
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 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) · Zbl 05837003 · doi:10.1007/978-3-642-16573-3_14
[2] Ammons, G., Bodik, R., Larus, J.: Mining specifications. In: Proc. 29th ACM Symp. on Principles of Programming Languages, pp. 4–16 (2002) · Zbl 1323.68361 · doi:10.1145/503272.503275
[3] Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75(2), 87–106 (1987) · Zbl 0636.68112 · doi:10.1016/0890-5401(87)90052-6
[4] Berg, T., Jonsson, B., Raffelt, H.: Regular Inference for State Machines Using Domains with Equality Tests. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 317–331. Springer, Heidelberg (2008) · Zbl 05270513 · doi:10.1007/978-3-540-78743-3_24
[5] Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems. LNCS, vol. 3472. Springer, Heidelberg (2005) · Zbl 1070.68088
[6] Cassel, S., Howar, F., Jonsson, B., Merten, M., Steffen, B.: A Succinct Canonical Register Automaton Model. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 366–380. Springer, Heidelberg (2011) · Zbl 1348.68095 · doi:10.1007/978-3-642-24372-1_26
[7] Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
[8] Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Science of Computer Programming 69(1-3), 35–45 (2007) · Zbl 1161.68390 · doi:10.1016/j.scico.2007.01.015
[9] Hagerer, A., Hungar, H., Niese, O., Steffen, B.: Model Generation by Moderated Regular Extrapolation. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 80–95. Springer, Heidelberg (2002) · Zbl 1059.68534 · doi:10.1007/3-540-45923-5_6
[10] Howar, F., Steffen, B., Merten, M.: Automata Learning with Automated Alphabet Abstraction Refinement. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 263–277. Springer, Heidelberg (2011) · Zbl 1317.68096 · doi:10.1007/978-3-642-18275-4_19
[11] Huima, A.: Implementing Conformiq Qtronic. In: Petrenko, A., Veanes, M., Tretmans, J., Grieskamp, W. (eds.) TestCom/FATES 2007. LNCS, vol. 4581, pp. 1–12. Springer, Heidelberg (2007) · Zbl 05293154 · doi:10.1007/978-3-540-73066-8_1
[12] Hungar, H., Niese, O., Steffen, B.: Domain-Specific Optimization in Automata Learning. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 315–327. Springer, Heidelberg (2003) · Zbl 1278.68177 · doi:10.1007/978-3-540-45069-6_31
[13] Jonsson, B., Parrow, J.: Deciding bisimulation equivalences for a class of non-finite-state programs. Information and Computation 107(2), 272–302 (1993) · Zbl 0799.68133 · doi:10.1006/inco.1993.1069
[14] Kaminski, M., Francez, N.: Finite-memory automata. Theoretical Computer Science 134(2), 329–363 (1994) · Zbl 0938.68711 · doi:10.1016/0304-3975(94)90242-9
[15] Lo, D., Maoz, S.: Scenario-based and value-based specification mining: better together. In: 25th IEEE/ACM Int. Conf. on Automated Software Engineering, ASE 2010, Antwerp, Belgium, pp. 387–396. ACM (2010) · doi:10.1145/1858996.1859081
[16] Lorenzoli, D., Mariani, L., Pezzè, M.: Automatic generation of software behavioral models. In: Proc. ICSE 2008: 30th Int. Conf. on Software Enginering, pp. 501–510 (2008) · doi:10.1145/1368088.1368157
[17] Mariani, L., Pezzé, M.: Dynamic detection of COTS components incompatibility. IEEE Software 24(5), 76–85 (2007) · Zbl 05335315 · doi:10.1109/MS.2007.138
[18] 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) · Zbl 05897407 · doi:10.1007/978-3-642-19835-9_18
[19] Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Information and Computation 103(2), 299–347 (1993) · Zbl 0786.68082 · doi:10.1006/inco.1993.1021
[20] Saint-Andre, P.: Extensible Messaging and Presence Protocol (XMPP): Instant Messaging and Presence. RFC 6121 (Proposed Standard) (March 2011)
[21] Sakamoto, H.: Learning Simple Deterministic Finite-Memory Automata. In: Li, M. (ed.) ALT 1997. LNCS, vol. 1316, pp. 416–431. Springer, Heidelberg (1997) · doi:10.1007/3-540-63577-7_58
[22] Shu, G., Lee, D.: Testing security properties of protocol implementations - a machine learning based approach. In: Proc. ICDCS 2007, 27th IEEE Int. Conf. on Distributed Computing Systems, Toronto, Ontario. IEEE Computer Society (2007)
[23] 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) · Zbl 05914420 · doi:10.1007/978-3-642-21455-4_8
[24] Tretmans, J.: Model-Based Testing and Some Steps towards Test-Based Modelling. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 297–326. Springer, Heidelberg (2011) · Zbl 05914421 · doi:10.1007/978-3-642-21455-4_9
[25] Wolper, P.: Expressing interesting properties of programs in propositional temporal logic (extended abstract). In: Proc. 13th ACM Symp. on Principles of Programming Languages, pp. 184–193 (January 1986)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.