{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T13:38:54Z","timestamp":1774964334119,"version":"3.50.1"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,4,1]],"date-time":"2016-04-01T00:00:00Z","timestamp":1459468800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2016,4]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            We present a black-box active learning algorithm for inferring extended finite state machines (EFSM)s by dynamic black-box analysis. EFSMs can be used to model both data flow and control behavior of software and hardware components. Different dialects of EFSMs are widely used in tools for model-based software development, verification, and testing. Our algorithm infers a class of EFSMs called\n            <jats:italic>register automata<\/jats:italic>\n            . Register automata have a finite control structure, extended with variables (registers), assignments, and guards. Our algorithm is parameterized on a particular\n            <jats:italic>theory<\/jats:italic>\n            , i.e., a set of operations and tests on the data domain that can be used in guards.\n          <\/jats:p>\n          <jats:p>\n            Key to our learning technique is a novel learning model based on so-called\n            <jats:italic>tree queries<\/jats:italic>\n            . The learning algorithm uses tree queries to infer symbolic data constraints on parameters, e.g., sequence numbers, time stamps, identifiers, or even simple arithmetic. We describe sufficient conditions for the properties that the symbolic constraints provided by a tree query in general must have to be usable in our learning model. We also show that, under these conditions, our framework induces a generalization of the classical Nerode equivalence and canonical automata construction to the symbolic setting. We have evaluated our algorithm in a black-box scenario, where tree queries are realized through (black-box) testing. Our case studies include connection establishment in TCP and a priority queue from the Java Class Library.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0355-5","type":"journal-article","created":{"date-parts":[[2016,2,12]],"date-time":"2016-02-12T12:49:57Z","timestamp":1455281397000},"page":"233-263","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":86,"title":["Active learning for extended finite state machines"],"prefix":"10.1145","volume":"28","author":[{"given":"Sofia","family":"Cassel","sequence":"first","affiliation":[{"name":"Department of Information Technology, Uppsala University, Uppsala, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Falk","family":"Howar","sequence":"additional","affiliation":[{"name":"IPSSE, TU Clausthal, Clausthal-Zellerfeld, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bengt","family":"Jonsson","sequence":"additional","affiliation":[{"name":"Department of Information Technology, Uppsala University, Uppsala, Sweden"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[{"name":"Chair for Programming Systems, TU Dortmund, Dortmund, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Ammons G Bod\u00edk R Larus JR (2002) Mining specifications. In: Proc. POPL 2002 pp 4\u201316. ACM","DOI":"10.1145\/565816.503275"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Alur R Cern\u00fd P Madhusudan P Nam W (2005) Synthesis of interface specifications for Java classes. In: Proc. POPL 2005 pp 98\u2013109. ACM","DOI":"10.1145\/1047659.1040314"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Aarts F Ruiter JD Poll E (2013) Formal models of bank cards for free. In: Proc. ICSTW 2013 pp 461\u2013468. IEEE","DOI":"10.1109\/ICSTW.2013.60"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Aarts F Heidarian F Kuppens H Olsen P Vaandrager FW (2012) Automata learning through counterexample guided abstraction refinement. In: Proc. FM 2012 volume 7436 of LNCS pp 10\u201327. Springer","DOI":"10.1007\/978-3-642-32759-9_4"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Aarts F Howar F Kuppens H Vaandrager FW (2014) Algorithms for inferring register automata\u2014a comparison of existing approaches. In: Proc. ISoLA 2014 Part I volume 8802 of LNCS pp 202\u2013219. Springer","DOI":"10.1007\/978-3-662-45234-9_15"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Aarts F Jonsson B Uijen J Vaandrager F (2014) Generating models of infinite-state communication protocols using regular inference with abstraction. Formal Methods Syst Design 46(1):1\u201341","DOI":"10.1007\/s10703-014-0216-x"},{"key":"e_1_2_1_2_7_2","unstructured":"Aarts F Kuppens H Tretmans J Vaandrager FW Verwer S (2012) Learning and testing the bounded retransmission protocol. In: Proc. ICGI 2012 volume 21 of JMLR Proceedings pp 4\u201318. JMLR.org"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(87)90052-6"},{"issue":"3","key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","first-page":"329","DOI":"10.1017\/S0960129504004153","article-title":"A channel-based coordination model for component composition","volume":"14","author":"Reo FA","year":"2004","journal-title":"Math Struct Comput Sci"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Aarts F Schmaltz J Vaandrager FW (2010) Inference and abstraction of the biometric passport. In: Proc. ISoLA 2010 Part I volume 6415 of LNCS pp 673\u2013686. Springer","DOI":"10.1007\/978-3-642-16558-0_54"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Botin\u010dan M Babi\u0107 D (2013) Sigma*: symbolic learning of input\u2013output specifications. In: Proc. POPL 2013 pp 443\u2013456. ACM","DOI":"10.1145\/2480359.2429123"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Ball T Bounimova E Cook B Levin V Lichtenberg J McGarvey C Ondrusek B Rajamani SK Ustuner A (2006) Thorough static analysis of device drivers. In: Proc. 2006 EuroSys Conf. pp 73\u201385. ACM","DOI":"10.1145\/1218063.1217943"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Bollig B Habermehl P Leucker M Monmege B (2013) A fresh approach to learning register automata. In: Proc. DLT 2013 volume 7907 of LNCS pp 118\u2013130. Springer","DOI":"10.1007\/978-3-642-38771-5_12"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Broy M Jonsson B Katoen J-P Leucker M Pretschner A (eds) (2004) Model-based testing of reactive systems volume 3472 of LNCS. Springer Berlin","DOI":"10.1007\/b137241"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Berg T Jonsson B Raffelt H (2008) Regular inference for state machines using domains with equality tests. In: Proc. FASE volume 4961 of LNCS pp 317\u2013331","DOI":"10.1007\/978-3-540-78743-3_24"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2009.12.002"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model checking","author":"Clarke E. M","year":"2001"},{"key":"e_1_2_1_2_18_2","unstructured":"Cassel S Howar F Jonsson B (2015) RALib: a LearnLib extension for inferring efsms. In: DIFTS 2015 Available online: http:\/\/www.faculty.ece.vt.edu\/chaowang\/difts2015\/papers\/paper_5.pdf."},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Cassel S Howar F Jonsson B Steffen B (2014) Learning extended finite state machines. In: Proc. SEFM 2014 volume 8702 of LNCS pp 250\u2013264. Springer","DOI":"10.1007\/978-3-319-10431-7_18"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Moura L. MD Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: Proc. TACAS 2008 volume 4963 of LNCS pp 337\u2013340. Springer","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.01.015"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Gery E Harel D Rhapsody EP (2002) A complete life-cycle model-based development system. In: Proc. IFM 2002 volume 2335 of LNCS pp 1\u201310. Springer","DOI":"10.1007\/3-540-47884-1_1"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Groz R Irfan M-N Oriat C (2012) Algorithmic improvements on regular inference of software models and perspectives for security testing. In: Proc. ISoLA 2012 Part I volume 7609 of LNCS pp 444\u2013457. Springer","DOI":"10.1007\/978-3-642-34026-0_33"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Giannakopoulou D Rakamari\u0107 Z Raman V (2012) Symbolic learning of component interfaces. In: Proc. SAS 2012 volume 7460 of LNCS pp 248\u2013264. Springer Berlin Heidelberg","DOI":"10.1007\/978-3-642-33125-1_18"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Hagerer A Hungar H Niese O Steffen B (2002) Model generation by moderated regular extrapolation. In: Proc. FASE 2002 volume 2306 of LNCS pp 80\u201395. Springer","DOI":"10.1007\/3-540-45923-5_6"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"crossref","unstructured":"Howar F Isberner M Steffen B Bauer O Jonsson B (2012) Inferring semantic interfaces of data structures. In: Proc. ISoLA 2012 Part I volume 7609 of LNCS pp 554\u2013571. Springer","DOI":"10.1007\/978-3-642-34026-0_41"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Henzinger TA Jhala R Majumdar R (2005) Permissive interfaces. In: Proc. ESEC\/FSE 2005 pp 31\u201340. ACM","DOI":"10.1145\/1095430.1081713"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Hungar H Niese O Steffen B (2003) Domain-specific optimization in automata learning. In: Proc. CAV 2003 volume 2725 of LNCS pp 315\u2013327. Springer","DOI":"10.1007\/978-3-540-45069-6_31"},{"key":"e_1_2_1_2_29_2","unstructured":"Howar F (2012) Active learning of interface programs. PhD thesis Technical University of Dortmund Germany 2012"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Howar F Steffen B Jonsson B Cassel S (2012) Inferring canonical register automata. In: Proc. VMCAI 2012 volume 7148 of LNCS pp 251\u2013266. Springer","DOI":"10.1007\/978-3-642-27940-9_17"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Howar F Steffen B Merten M (2011) Automata learning with automated alphabet abstraction refinement. In: Proc. VMCAI 2011 volume 6538 of LNCS pp 263\u2013277. Springer","DOI":"10.1007\/978-3-642-18275-4_19"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Huima A (2007) Implementing Conformiq Qtronic. In: Proc. TestCom\/FATES 2007 volume 4581 of LNCS pp 1\u201312. Springer","DOI":"10.1007\/978-3-540-73066-8_1"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10994-013-5419-7"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Isberner M Howar F Steffen B (2015) The open-source learnlib\u2014a framework for active automata learning. In: Kroening D Pasareanu CS (eds) Proc. CAV 2015 volume 9206 of LNCS pp 487\u2013495. Springer","DOI":"10.1007\/978-3-319-21690-4_32"},{"issue":"4","key":"e_1_2_1_2_35_2","doi-asserted-by":"crossref","first-page":"21, 1","DOI":"10.1145\/1592434.1592438","article-title":"Software model checking","volume":"41","author":"Jhala R","year":"2009","journal-title":"ACM Comput Surv"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Lorenzoli D Mariani L Pezz\u00e8 M (2008) Automatic generation of software behavioral models. In: Proc. ICSE 2008 pp 501\u2013510. ACM","DOI":"10.1145\/1368088.1368157"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"Maler O Mens I-E (2014) Learning regular languages over large alphabets. In: Proc. TACAS 2014 volume 8413 of LNCS pp 485\u2013499. Springer","DOI":"10.1007\/978-3-642-54862-8_41"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1021"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"crossref","unstructured":"Shu G Lee D (2007) Testing security properties of protocol implementations\u2014a machine learning based approach. In: Proc. ICDCS 2007 pp 25. IEEE","DOI":"10.1109\/ICDCS.2007.147"},{"key":"e_1_2_1_2_40_2","volume-title":"Practical model-based testing\u2014a tools approach","author":"Utting M","year":"2007"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Walkinshaw N Bogdanov K Derrick J Paris J (2010) Increasing functional coverage by inductive testing: a case study. In: Proc. ICTSS 2010 volume 6435 of LNCS pp 126\u2013141. Springer","DOI":"10.1007\/978-3-642-16573-3_10"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Xiao H Sun J Liu Y Lin S-W Sun C (2013) Tzuyu: learning stateful typestates. In: Proc. ASE 2013 pp 432\u2013442. IEEE","DOI":"10.1109\/ASE.2013.6693101"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0355-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0355-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0355-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:54:34Z","timestamp":1641538474000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0355-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4]]},"references-count":42,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,4]]}},"alternative-id":["10.1007\/s00165-016-0355-5"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0355-5","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4]]}}}