{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T03:58:33Z","timestamp":1782878313227,"version":"3.54.5"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415390","type":"print"},{"value":"9783319415406","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41540-6_25","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:07Z","timestamp":1468316047000},"page":"454-471","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":89,"title":["Combining Model Learning and Model Checking to Analyze TCP Implementations"],"prefix":"10.1007","author":[{"given":"Paul","family":"Fiter\u0103u-Bro\u015ftean","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ramon","family":"Janssen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"key":"25_CR1","unstructured":"Aarts, F.: Tomte: Bridging the Gap between Active Learning and Real-World Systems. Ph.D. thesis, Radboud University Nijmegen, October 2014"},{"issue":"1","key":"25_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-014-0216-x","volume":"46","author":"F Aarts","year":"2015","unstructured":"Aarts, F., Jonsson, B., Uijen, J., Vaandrager, F.W.: Generating models of infinite-state communication protocols using regular inference with abstraction. Formal Methods Syst. Des. 46(1), 1\u201341 (2015)","journal-title":"Formal Methods Syst. Des."},{"key":"25_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-642-15375-4_6","volume-title":"CONCUR 2010 - Concurrency Theory","author":"F Aarts","year":"2010","unstructured":"Aarts, F., Vaandrager, F.: Learning I\/O automata. In: Gastin, P., Laroussinie, F. (eds.) CONCUR 2010. LNCS, vol. 6269, pp. 71\u201385. Springer, Heidelberg (2010)"},{"key":"25_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-319-25150-9_11","volume-title":"Theoretical Aspects of Computing - ICTAC 2015","author":"F Aarts","year":"2015","unstructured":"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\u2013183. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-25150-9_11"},{"issue":"1","key":"25_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-014-0216-x","volume":"46","author":"F Aarts","year":"2015","unstructured":"Aarts, F., Jonsson, B., Uijen, J., Vaandrager, F.W.: Generat-ing models of infinite-state communication protocols using regular inference withabstraction. Formal Methods Syst. Des. 46(1), 1\u201341 (2015)","journal-title":"Formal Methods Syst. Des."},{"issue":"2","key":"25_CR6","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"25_CR7","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"issue":"3","key":"25_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1952522.1952527","volume":"10","author":"J Berendsen","year":"2011","unstructured":"Berendsen, J., Gebremichael, B., Vaandrager, F.W., Zhang, M.: Formal specification and analysis of Zeroconf using Uppaal. ACM Trans. Embed. Comput. Syst. 10(3), 1\u201332 (2011)","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"Braden, R.: RFC 1122 Requirements for Internet Hosts - Communication Layers. Internet Engineering Task Force, October 1989","DOI":"10.17487\/rfc1122"},{"key":"25_CR10","unstructured":"Brinksma, E., Mader, A.: On verification modelling of embedded systems. Technical report TR-CTIT-04-03, Centre for Telematics and Information Technology, Univ. of Twente, The Netherlands, January 2004"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Bruns, G., Staskauskas, M.G.: Applying formal methods to a protocol standard and its implementations. In: Proceedings International Symposium on Software Engineering for Parallel and Distributed Systems (PDSE 1998), 20\u201321 April 1998, Kyoto, Japan, pp. 198\u2013205. IEEE Computer Society (1998)","DOI":"10.1109\/PDSE.1998.668180"},{"key":"25_CR12","unstructured":"Cassel, S.: Learning Component Behavior from Tests: Theory and Algorithms for Automata with Data. Ph.D. thesis, University of Uppsala (2015)"},{"key":"25_CR13","unstructured":"Chalupar, G., Peherstorfer, S., Poll, E., de Ruiter, J.: Automated reverse engineering using Lego. In: Proceedings 8th USENIX Workshop on Offensive Technologies (WOOT 2014), San Diego, California, Los Alamitos, CA, USA, IEEE Computer Society, August 2014"},{"key":"25_CR14","doi-asserted-by":"crossref","unstructured":"Cho, C.Y., Babic, D., Shin, E.C.R., Song, D.: Inference and analysis of formal models of botnet command and control protocols. In: Al-Shaer, E., Keromytis, A.D., Shmatikov, V. (eds.) ACM Conference on Computer and Communications Security, pp. 426\u2013439. ACM (2010)","DOI":"10.1145\/1866307.1866355"},{"key":"25_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359\u2013364. Springer, Heidelberg (2002)"},{"issue":"5","key":"25_CR16","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003)","journal-title":"J. ACM"},{"key":"25_CR17","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"25_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1007\/978-3-319-10702-8_6","volume-title":"Formal Methods for Industrial Critical Systems","author":"P Fiter\u0103u-Bro\u015ftean","year":"2014","unstructured":"Fiter\u0103u-Bro\u015ftean, P., Janssen, R., Vaandrager, F.: Learning fragments of the TCP network protocol. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 78\u201393. Springer, Heidelberg (2014)"},{"issue":"47","key":"25_CR19","doi-asserted-by":"publisher","first-page":"4029","DOI":"10.1016\/j.tcs.2010.07.008","volume":"411","author":"O Grinchtein","year":"2010","unstructured":"Grinchtein, O., Jonsson, B., Leucker, M.: Learning of event-recording automata. Theor. Comput. Sci. 411(47), 4029\u20134054 (2010)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"25_CR20","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16(3), 843\u2013871 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"25_CR21","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual. Addison Wesley, Reading (2004)"},{"key":"25_CR22","unstructured":"Impacket. http:\/\/www.coresecurity.com\/corelabs-research\/open-source-tools\/impacket . Accessed 28 Jan 2016"},{"key":"25_CR23","unstructured":"Isberner, M: Foundations of Active Automata Learning: An Algorithmic Perspective. Ph.D. thesis, Technical University of Dortmund (2015)"},{"issue":"4","key":"25_CR24","doi-asserted-by":"publisher","first-page":"21:1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala, R., Majumdar, R.: Software model checking. ACM Comput. Surv. 41(4), 21:1\u201321:54 (2009)","journal-title":"ACM Comput. Surv."},{"issue":"7","key":"25_CR25","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"van Langevelde, I., Romijn, J.M.T., Goga, N.: Founding FireWire bridges through Promela prototyping. In: 8thInternational Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA). IEEE Computer Society Press, April 2003","DOI":"10.1109\/IPDPS.2003.1213434"},{"issue":"8","key":"25_CR27","doi-asserted-by":"publisher","first-page":"1090","DOI":"10.1109\/5.533956","volume":"84","author":"D Lee","year":"1996","unstructured":"Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines \u2013 a survey. Proc. IEEE 84(8), 1090\u20131123 (1996)","journal-title":"Proc. IEEE"},{"key":"25_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/978-3-319-10702-8_5","volume-title":"Formal Methods for Industrial Critical Systems","author":"L Lockefeer","year":"2014","unstructured":"Lockefeer, L., Williams, D.M., Fokkink, W.J.: Formal specification and verification of TCP extended with the window scale option. In: Lang, F., Flammini, F. (eds.) FMICS 2014. LNCS, vol. 8718, pp. 63\u201377. Springer, Heidelberg (2014)"},{"issue":"1","key":"25_CR29","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1007\/BF01384313","volume":"6","author":"C Loiseaux","year":"1995","unstructured":"Loiseaux, C., Graf, S., Sifakis, J., Boujjani, A., Bensalem, S.: Property preserving abstractions for the verification of concurrent systems. Formal Methods Syst. Des. 6(1), 11\u201344 (1995)","journal-title":"Formal Methods Syst. Des."},{"key":"25_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-642-21768-5_11","volume-title":"tests and proofs","author":"K Meinke","year":"2011","unstructured":"Meinke, K., Sindhu, M.A.: Incremental learning-based testing for reactive systems. In: Gogolla, M., Wolff, B. (eds.) TAP 2011. LNCS, vol. 6706, pp. 134\u2013151. Springer, Heidelberg (2011)"},{"key":"25_CR31","unstructured":"Musuvathi, M., Engler, D.R.: Model checking large network protocol implementations. In: Morris, R., Savage, S. (eds.) 1st Symposium on Networked Systems Design and Implementation (NSDI 2004), March 29\u201331, 2004, San Francisco, California, USA, Proceedings, pp. 155\u2013168. USENIX (2004)"},{"key":"25_CR32","unstructured":"Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: A pragmatic approach to model checking real code. In: Culler, D.E., Druschel, P. (eds.) 5th Symposium on Operating System Design and Implementation (OSDI 2002), Boston, Massachusetts, USA, December 9\u201311, 2002. USENIX Association (2002)"},{"issue":"4","key":"25_CR33","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1090\/S0002-9939-1958-0135681-9","volume":"9","author":"A Nerode","year":"1958","unstructured":"Nerode, A.: Linear automaton transformations. Proc. Am. Math. Soc. 9(4), 541\u2013544 (1958)","journal-title":"Proc. Am. Math. Soc."},{"key":"25_CR34","doi-asserted-by":"crossref","unstructured":"Paxson, V., Allman, M., Dawson, S., Fenner, W., Griner, J., Heavens, I., Lahey, K., Semke, J., Volz, B.: Known TCP Implementation Problems. RFC 2525 (Informational), March 1999","DOI":"10.17487\/rfc2525"},{"key":"25_CR35","unstructured":"Pcapy. http:\/\/www.coresecurity.com\/corelabs-research\/open-source-tools\/pcapy . Accessed 28 Jan 2016"},{"issue":"2","key":"25_CR36","first-page":"225","volume":"7","author":"D Peled","year":"2002","unstructured":"Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. J. Autom. Lang. Comb. 7(2), 225\u2013246 (2002)","journal-title":"J. Autom. Lang. Comb."},{"key":"25_CR37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-4177-9","volume-title":"Logik der Forschung","author":"KR Popper","year":"1935","unstructured":"Popper, K.R.: Logik der Forschung. Julius Springer Verlag, Vienna (1935)"},{"key":"25_CR38","doi-asserted-by":"crossref","unstructured":"Postel, J.: Transmission control protocol. RFC 793 (Standard), Updated by RFCs 1122, 3168, September 1981","DOI":"10.17487\/rfc0793"},{"issue":"5","key":"25_CR39","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/s10009-009-0111-8","volume":"11","author":"H Raffelt","year":"2009","unstructured":"Raffelt, H., Steffen, B., Berg, T., Margaria, T.: LearnLib: a framework for extrapolating behavioral models. STTT 11(5), 393\u2013407 (2009)","journal-title":"STTT"},{"key":"25_CR40","unstructured":"de Ruiter, J., Poll, E.: Protocol state fuzzing of tls implementations. In: 24th USENIX Security Symposium (USENIX Security 15), pp. 193\u2013206. SENIX Association, Washington, D.C., August 2015"},{"key":"25_CR41","unstructured":"Scapy. http:\/\/www.secdev.org\/projects\/scapy\/ . Accessed 28 Jan 2016"},{"issue":"4","key":"25_CR42","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1002\/stvr.1491","volume":"24","author":"M Shahbaz","year":"2014","unstructured":"Shahbaz, M., Groz, R.: Analysis and testing of black-box component-based systems by inferring partial models. Softw. Test. Verif. Reliab. 24(4), 253\u2013288 (2014)","journal-title":"Softw. Test. Verif. Reliab."},{"key":"25_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-319-25423-4_5","volume-title":"Formal Methods and Software Engineering","author":"W Smeenk","year":"2015","unstructured":"Smeenk, W., Moerman, J., Vaandrager, F., Jansen, D.N.: Applying automata learning to embedded control software. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 67\u201383. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-25423-4_5"},{"key":"25_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-21455-4_8","volume-title":"Formal Methods for Eternal Networked Software Systems","author":"B Steffen","year":"2011","unstructured":"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\u2013296. Springer, Heidelberg (2011)"},{"issue":"3","key":"25_CR45","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s001650300009","volume":"14","author":"M Stoelinga","year":"2003","unstructured":"Stoelinga, M.: Fun with FireWire: A comparative study of formal verification methods applied to the IEEE 1394 root contention protocol. Formal Aspects Comput. J. 14(3), 328\u2013337 (2003)","journal-title":"Formal Aspects Comput. J."},{"key":"25_CR46","unstructured":"Verleg, P.: Inferring SSH state machines using protocol state fuzzing. Master thesis, Radboud University (2016)"},{"key":"25_CR47","unstructured":"Verwer, S.: Efficient Identification of Timed Automata \u2013 Theory and Practice. Ph.D. thesis, Delft University of Technology, March 2010"},{"key":"25_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1007\/978-3-662-45234-9_16","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"M Volpato","year":"2014","unstructured":"Volpato, M., Tretmans, J.: Active learning of nondeterministic systems from an ioco perspective. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014, Part I. LNCS, vol. 8802, pp. 220\u2013235. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41540-6_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T00:41:47Z","timestamp":1748997707000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41540-6_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415390","9783319415406"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41540-6_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}