Bib for the applying paper

biblio-web.bib

@@ -2,5 +2,15 @@
 	author    = {Michal Szynwelski},
 	title     = {{N}\lambda},
 	note      = {Website},
-	url       = {http://www.mimuw.edu.pl/~szynwelski/nlambda/}
+	url       = {http://www.mimuw.edu.pl/~szynwelski/nlambda/},
+	urldate   = {2018-08-14}
+}
+
+@misc{OMGUML2,
+	author    = {Object Management Group ({OMG})},
+	title     = {Unified modeling language specification: Version 2, revised final adopted specification}
+	note      = {Website},
+	url       = {http://www.uml.org/#UML2.0},
+	year      = {2004},
+	urldate   = {2012-07-23}
 }

biblio.bib

@@ -31,6 +31,36 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@phdthesis{Aarts14,
+	title     = {Tomte: bridging the gap between active learning and real-world systems},
+	author    = {Fides Dorothea Aarts},
+	year      = {2014},
+	isbn      = {978-90-9028499-6}
+	publisher = {[Sl: sn]},
+	series    = {IPA dissertation series; 2014-12},
+	school    = {Radboud University, Nijmegen, The Netherlands},
+	url       = {http://hdl.handle.net/2066/130428}
+}
+
+@article{DBLP:journals/ml/AartsKTVV14,
+	author    = {Fides Aarts and
+	             Harco Kuppens and
+	             Jan Tretmans and
+	             Frits W. Vaandrager and
+	             Sicco Verwer},
+	title     = {Improving active {M}ealy machine learning for protocol conformance testing},
+	journal   = {Machine Learning},
+	volume    = {96},
+	number    = {1-2},
+	pages     = {189--224},
+	year      = {2014},
+	url       = {https://doi.org/10.1007/s10994-013-5405-0},
+	doi       = {10.1007/s10994-013-5405-0},
+	timestamp = {Tue, 26 Jun 2018 14:09:25 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/ml/AartsKTVV14},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @inproceedings{DBLP:conf/ictac/AartsFKV15,
 	author    = {Fides Aarts and
 	             Paul Fiterau{-}Brostean and
@@ -67,6 +97,25 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{DBLP:journals/fmsd/AartsJUV15,
+	author    = {Fides Aarts and
+	             Bengt Jonsson and
+	             Johan Uijen and
+	             Frits W. Vaandrager},
+	title     = {Generating models of infinite-state communication protocols using
+	             regular inference with abstraction},
+	journal   = {Formal Methods in System Design},
+	volume    = {46},
+	number    = {1},
+	pages     = {1--41},
+	year      = {2015},
+	url       = {https://doi.org/10.1007/s10703-014-0216-x},
+	doi       = {10.1007/s10703-014-0216-x},
+	timestamp = {Sat, 27 May 2017 14:24:05 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/fmsd/AartsJUV15},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{DBLP:journals/iandc/Angluin87,
 	author    = {Dana Angluin},
 	title     = {Learning Regular Sets from Queries and Counterexamples},
@@ -142,6 +191,48 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DBLP:conf/icwsm/BastianHJ09,
+	author    = {Mathieu Bastian and
+	             Sebastien Heymann and
+	             Mathieu Jacomy},
+	editor    = {Eytan Adar and
+	             Matthew Hurst and
+	             Tim Finin and
+	             Natalie S. Glance and
+	             Nicolas Nicolov and
+	             Belle L. Tseng},
+	title     = {Gephi: An Open Source Software for Exploring and Manipulating Networks},
+	booktitle = {Proceedings of the Third International Conference on Weblogs and Social
+	             Media, {ICWSM} 2009, San Jose, California, USA, May 17-20, 2009},
+	publisher = {The {AAAI} Press},
+	year      = {2009},
+	url       = {http://aaai.org/ocs/index.php/ICWSM/09/paper/view/154},
+	timestamp = {Thu, 13 Dec 2012 14:15:16 +0100},
+	biburl    = {https://dblp.org/rec/bib/conf/icwsm/BastianHJ09},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/qest/BehrmannDLHPYH06,
+	author    = {Gerd Behrmann and
+	             Alexandre David and
+	             Kim Guldstrand Larsen and
+	             John H{\aa}kansson and
+	             Paul Pettersson and
+	             Wang Yi and
+	             Martijn Hendriks},
+	title     = {{UPPAAL} 4.0},
+	booktitle = {Third International Conference on the Quantitative Evaluation of Systems
+	             {(QEST} 2006), 11-14 September 2006, Riverside, California, {USA}},
+	pages     = {125--126},
+	publisher = {{IEEE} Computer Society},
+	year      = {2006},
+	url       = {https://doi.org/10.1109/QEST.2006.59},
+	doi       = {10.1109/QEST.2006.59},
+	timestamp = {Fri, 26 May 2017 00:51:19 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/qest/BehrmannDLHPYH06},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @inproceedings{DBLP:conf/fase/BergGJLRS05,
 	author    = {Therese Berg and
 	             Olga Grinchtein and
@@ -478,6 +569,25 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{DBLP:journals/jlp/CasselHJMS15,
+	author    = {Sofia Cassel and
+	             Falk Howar and
+	             Bengt Jonsson and
+	             Maik Merten and
+	             Bernhard Steffen},
+	title     = {A succinct canonical register automaton model},
+	journal   = {J. Log. Algebr. Meth. Program.},
+	volume    = {84},
+	number    = {1},
+	pages     = {54--66},
+	year      = {2015},
+	url       = {https://doi.org/10.1016/j.jlamp.2014.07.004},
+	doi       = {10.1016/j.jlamp.2014.07.004},
+	timestamp = {Sun, 28 May 2017 13:17:34 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/jlp/CasselHJMS15},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{DBLP:journals/fac/CasselHJS16,
 	author    = {Sofia Cassel and
 	             Falk Howar and
@@ -528,6 +638,38 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DBLP:conf/ccs/ChocSS10,
+	author    = {Chia Yuan Cho and
+	             Domagoj Babic and
+	             Eui Chul Richard Shin and
+	             Dawn Song},
+	title     = {Inference and analysis of formal models of botnet command and control protocols},
+	booktitle = {Proceedings of the 17th {ACM} Conference on Computer and Communications
+	             Security, {CCS} 2010, Chicago, Illinois, USA, October 4-8, 2010},
+	pages     = {426--439},
+	year      = {2010},
+	crossref  = {DBLP:conf/ccs/2010},
+	url       = {http://doi.acm.org/10.1145/1866307.1866355},
+	doi       = {10.1145/1866307.1866355},
+	timestamp = {Tue, 23 Nov 2010 21:55:35 +0100},
+	biburl    = {https://dblp.org/rec/bib/conf/ccs/ChocSS10},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@proceedings{DBLP:conf/ccs/2010,
+	editor    = {Ehab Al{-}Shaer and
+	             Angelos D. Keromytis and
+	             Vitaly Shmatikov},
+	title     = {Proceedings of the 17th {ACM} Conference on Computer and Communications
+	             Security, {CCS} 2010, Chicago, Illinois, USA, October 4-8, 2010},
+	publisher = {{ACM}},
+	year      = {2010},
+	isbn      = {978-1-4503-0245-6},
+	timestamp = {Mon, 22 Nov 2010 20:51:09 +0100},
+	biburl    = {https://dblp.org/rec/bib/conf/ccs/2010},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{DBLP:journals/tse/Chow78,
 	author    = {Tsun S. Chow},
 	title     = {Testing Software Design Modeled by Finite-State Machines},
@@ -559,6 +701,29 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DBLP:conf/fase/DavidMY02,
+	author    = {Alexandre David and
+	             M. Oliver M{\"{o}}ller and
+	             Wang Yi},
+	editor    = {Ralf-Detlef Kutsche and
+	             Herbert Weber},
+	title     = {Formal Verification of {UML} Statecharts with Real-Time Extensions},
+	booktitle = {Fundamental Approaches to Software Engineering, 5th International
+	             Conference, {FASE} 2002, held as Part of the Joint European Conferences
+	             on Theory and Practice of Software, {ETAPS} 2002, Grenoble, France,
+	             April 8-12, 2002, Proceedings},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {2306},
+	pages     = {218--232},
+	publisher = {Springer},
+	year      = {2002},
+	url       = {https://doi.org/10.1007/3-540-45923-5\_15},
+	doi       = {10.1007/3-540-45923-5\_15},
+	timestamp = {Fri, 26 May 2017 14:09:14 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/fase/DavidMY02},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{DBLP:journals/tocl/DemriL09,
 	author    = {St{\'{e}}phane Demri and
 	             Ranko Lazic},
@@ -627,6 +792,45 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@article{DBLP:journals/re/EshuisJW02,
+	author    = {Rik Eshuis and
+	             David N. Jansen and
+	             Roel Wieringa},
+	title     = {Requirements-Level Semantics and Model Checking of Object-Oriented Statecharts},
+	journal   = {Requir. Eng.},
+	volume    = {7},
+	number    = {4},
+	pages     = {243--263},
+	year      = {2002},
+	url       = {https://doi.org/10.1007/s007660200019},
+	doi       = {10.1007/s007660200019},
+	timestamp = {Sat, 20 May 2017 00:26:07 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/re/EshuisJW02},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/fmics/Fiterau-BrosteanJV14,
+	author    = {Paul Fiterau{-}Brostean and
+	             Ramon Janssen and
+	             Frits W. Vaandrager},
+	editor    = {Fr{\'{e}}d{\'{e}}ric Lang and
+	             Francesco Flammini},
+	title     = {Learning Fragments of the {TCP} Network Protocol},
+	booktitle = {Formal Methods for Industrial Critical Systems - 19th International
+	             Conference, {FMICS} 2014, Florence, Italy, September 11-12, 2014.
+	             Proceedings},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {8718},
+	pages     = {78--93},
+	publisher = {Springer},
+	year      = {2014},
+	url       = {https://doi.org/10.1007/978-3-319-10702-8\_6},
+	doi       = {10.1007/978-3-319-10702-8\_6},
+	timestamp = {Sat, 16 Sep 2017 12:12:00 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/fmics/Fiterau-BrosteanJV14},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @inproceedings{DBLP:conf/cav/Fiterau-Brostean16,
 	author    = {Paul Fiterau{-}Brostean and
 	             Ramon Janssen and
@@ -680,6 +884,116 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DBLP:conf/tacas/GaravelLMS11,
+	author    = {Hubert Garavel and
+	             Fr{\'{e}}d{\'{e}}ric Lang and
+	             Radu Mateescu and
+	             Wendelin Serwe},
+	editor    = {Parosh Aziz Abdulla and
+	             K. Rustan M. Leino},
+	title     = {{CADP} 2010: {A} Toolbox for the Construction and Analysis of Distributed
+	             Processes},
+	booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
+	             - 17th International Conference, {TACAS} 2011, Held as Part of the
+	             Joint European Conferences on Theory and Practice of Software, {ETAPS}
+	             2011, Saarbr{\"{u}}cken, Germany, March 26-April 3, 2011. Proceedings},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {6605},
+	pages     = {372--387},
+	publisher = {Springer},
+	year      = {2011},
+	url       = {https://doi.org/10.1007/978-3-642-19835-9\_33},
+	doi       = {10.1007/978-3-642-19835-9\_33},
+	timestamp = {Tue, 26 Jun 2018 14:11:56 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/tacas/GaravelLMS11},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/mompes/GraafD07,
+	author    = {Bas Graaf and
+	             Arie van Deursen},
+	editor    = {Jo{\~{a}}o M. Fernandes and
+	             Ricardo Jorge Machado and
+	             Ridha Kh{\'{e}}dri and
+	             Siobh{\'{a}}n Clarke},
+	title     = {Model-Driven Consistency Checking of Behavioural Specifications},
+	booktitle = {Model-based Methodologies for Pervasive and Embedded Software, 4th
+	             International Workshop on Model-based Methodologies for Pervasive and
+	             Embedded Software, {MOMPES} 2007, Braga, Portugal, March 31, 2007, Proceedings},
+	pages     = {115--126},
+	publisher = {{IEEE} Computer Society},
+	year      = {2007},
+	url       = {https://doi.org/10.1109/MOMPES.2007.12},
+	doi       = {10.1109/MOMPES.2007.12},
+	timestamp = {Thu, 15 Jun 2017 21:44:48 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/mompes/GraafD07},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/pts/GrozLPS08,
+	author    = {Roland Groz and
+	             Keqin Li and
+	             Alexandre Petrenko and
+	             Muzammil Shahbaz},
+	editor    = {Kenji Suzuki and
+	             Teruo Higashino and
+	             Andreas Ulrich and
+	             Toru Hasegawa},
+	title     = {Modular System Verification by Inference, Testing and Reachability
+	             Analysis},
+	booktitle = {Testing of Software and Communicating Systems, 20th {IFIP} {TC} 6/WG
+	             6.1 International Conference, TestCom 2008, 8th International Workshop,
+	             {FATES} 2008, Tokyo, Japan, June 10-13, 2008, Proceedings},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {5047},
+	pages     = {216--233},
+	publisher = {Springer},
+	year      = {2008},
+	url       = {https://doi.org/10.1007/978-3-540-68524-1\_16},
+	doi       = {10.1007/978-3-540-68524-1\_16},
+	timestamp = {Tue, 26 Jun 2018 14:11:07 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/pts/GrozLPS08},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/fmco/HansenKLMPS10,
+	author    = {Helle Hvid Hansen and
+	             Jeroen Ketema and
+	             Bas Luttik and
+	             Mohammad Reza Mousavi and
+	             Jaco van de Pol and
+	             Osmar Marchi dos Santos},
+	title     = {Automated Verification of Executable {UML} Models},
+	booktitle = {Formal Methods for Components and Objects - 9th International Symposium,
+	             {FMCO} 2010, Graz, Austria, November 29 - December 1, 2010. Revised Papers},
+	pages     = {225--250},
+	year      = {2010},
+	crossref  = {DBLP:conf/fmco/2010},
+	url       = {https://doi.org/10.1007/978-3-642-25271-6\_12},
+	doi       = {10.1007/978-3-642-25271-6\_12},
+	timestamp = {Fri, 02 Jun 2017 20:50:15 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/fmco/HansenKLMPS10},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@proceedings{DBLP:conf/fmco/2010,
+	editor    = {Bernhard K. Aichernig and
+	             Frank S. de Boer and
+	             Marcello M. Bonsangue},
+	title     = {Formal Methods for Components and Objects - 9th International Symposium,
+	             {FMCO} 2010, Graz, Austria, November 29 - December 1, 2010. Revised Papers},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {6957},
+	publisher = {Springer},
+	year      = {2012},
+	url       = {https://doi.org/10.1007/978-3-642-25271-6},
+	doi       = {10.1007/978-3-642-25271-6},
+	isbn      = {978-3-642-25270-9},
+	timestamp = {Wed, 17 May 2017 14:24:49 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/fmco/2010},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{DBLP:journals/cj/HieronsT15,
 	author    = {Robert M. Hierons and
 	             Uraz Cengiz T{\"{u}}rker},
@@ -696,6 +1010,16 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@book{Higuera10,
+	author    = {Colin de la Higuera},
+	publisher = {Cambridge University Press},
+	title     = {Grammatical Inference: Learning Automata and Grammars},
+	year      = {2010},
+	isbn      = {9781139194655},
+	doi       = {10.1017/CBO9781139194655},
+	url       = {https://doi.org/10.1017/CBO9781139194655}
+}
+
 @inproceedings{DBLP:conf/vmcai/HowarSM11,
 	author    = {Falk Howar and
 	             Bernhard Steffen and
@@ -765,6 +1089,27 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DBLP:conf/cav/HungarNS03,
+	author    = {Hardi Hungar and
+	             Oliver Niese and
+	             Bernhard Steffen},
+	editor    = {Warren A. Hunt Jr. and
+	             Fabio Somenzi},
+	title     = {Domain-Specific Optimization in Automata Learning},
+	booktitle = {Computer Aided Verification, 15th International Conference, {CAV}
+	             2003, Boulder, CO, USA, July 8-12, 2003, Proceedings},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {2725},
+	pages     = {315--327},
+	publisher = {Springer},
+	year      = {2003},
+	url       = {https://doi.org/10.1007/978-3-540-45069-6\_31},
+	doi       = {10.1007/978-3-540-45069-6\_31},
+	timestamp = {Mon, 29 May 2017 16:53:43 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/cav/HungarNS03},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @inproceedings{DBLP:conf/nfm/IsbernerHS13,
 	author    = {Malte Isberner and
 	             Falk Howar and
@@ -999,6 +1344,64 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DBLP:conf/fmco/KrennSA09,
+	author    = {Willibald Krenn and
+	             Rupert Schlick and
+	             Bernhard K. Aichernig},
+	title     = {Mapping {UML} to Labeled Transition Systems for Test-Case Generation
+	             - {A} Translation via Object-Oriented Action Systems},
+	booktitle = {Formal Methods for Components and Objects - 8th International Symposium,
+	             {FMCO} 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised
+	             Selected Papers},
+	pages     = {186--207},
+	year      = {2009},
+	crossref  = {DBLP:conf/fmco/2009},
+	url       = {https://doi.org/10.1007/978-3-642-17071-3\_10},
+	doi       = {10.1007/978-3-642-17071-3\_10},
+	timestamp = {Fri, 02 Jun 2017 20:50:15 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/fmco/KrennSA09},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@proceedings{DBLP:conf/fmco/2009,
+	editor    = {Frank S. de Boer and
+	             Marcello M. Bonsangue and
+	             Stefan Hallerstede and
+	             Michael Leuschel},
+	title     = {Formal Methods for Components and Objects - 8th International Symposium,
+	             {FMCO} 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised
+	             Selected Papers},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {6286},
+	publisher = {Springer},
+	year      = {2010},
+	url       = {https://doi.org/10.1007/978-3-642-17071-3},
+	doi       = {10.1007/978-3-642-17071-3},
+	isbn      = {978-3-642-17070-6},
+	timestamp = {Wed, 17 May 2017 14:24:49 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/fmco/2009},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{LanusseTEMGTSDT09,
+	title     = {Papyrus {UML}: an open source toolset for {MDA}},
+	author    = {Agnes Lanusse and
+	             Yann Tanguy and
+	             Huascar Espinoza and
+	             Chokri Mraidha and
+	             Sebastien Gerard and
+	             Patrick Tessier and
+	             Remi Schnekenburger and
+	             Hubert Dubois and
+	             Fran{\c{c}}ois Terrier},
+	editor    = {Regis Vogel}
+	booktitle = {Proc. of the Fifth European Conference on Model-Driven Architecture Foundations and Applications (ECMDA-FA 2009)},
+	pages     = {1--4},
+	year      = {2009},
+	publisher = {CTIT},
+	series    = {CTIT Proceedings Series WP09-12}
+}
+
 @article{DBLP:journals/tc/LeeY94,
 	author    = {David Lee and
 	             Mihalis Yannakakis},
@@ -1015,6 +1418,64 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DBLP:conf/fmco/Leucker06,
+	author    = {Martin Leucker},
+	title     = {Learning Meets Verification},
+	booktitle = {Formal Methods for Components and Objects, 5th International Symposium,
+	             {FMCO} 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures},
+	pages     = {127--151},
+	year      = {2006},
+	crossref  = {DBLP:conf/fmco/2006},
+	url       = {https://doi.org/10.1007/978-3-540-74792-5\_6},
+	doi       = {10.1007/978-3-540-74792-5\_6},
+	timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/fmco/Leucker06},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@proceedings{DBLP:conf/fmco/2006,
+	editor    = {Frank S. de Boer and
+	             Marcello M. Bonsangue and
+	             Susanne Graf and
+	             Willem P. de Roever},
+	title     = {Formal Methods for Components and Objects, 5th International Symposium,
+	             {FMCO} 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {4709},
+	publisher = {Springer},
+	year      = {2007},
+	url       = {https://doi.org/10.1007/978-3-540-74792-5},
+	doi       = {10.1007/978-3-540-74792-5},
+	isbn      = {978-3-540-74791-8},
+	timestamp = {Fri, 02 Jun 2017 13:01:07 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/fmco/2006},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/forte/LiGS06,
+	author    = {Keqin Li and
+	             Roland Groz and
+	             Muzammil Shahbaz},
+	editor    = {Elie Najm and
+	             Jean-Fran{\c{c}}ois Pradat-Peyre and
+	             V{\'{e}}ronique Donzeau-Gouge},
+	title     = {Integration Testing of Distributed Components Based on Learning Parameterized
+	             {I/O} Models},
+	booktitle = {Formal Techniques for Networked and Distributed Systems - {FORTE}
+	             2006, 26th {IFIP} {WG} 6.1 International Conference, Paris, France,
+	             September 26-29, 2006.},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {4229},
+	pages     = {436--450},
+	publisher = {Springer},
+	year      = {2006},
+	url       = {https://doi.org/10.1007/11888116\_31},
+	doi       = {10.1007/11888116\_31},
+	timestamp = {Tue, 26 Jun 2018 14:10:58 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/forte/LiGS06},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{LuoPB95,
 	author    = {Gang Luo and
 	             Alexandre Petrenko and
@@ -1060,6 +1521,31 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DBLP:conf/tacas/MertenHSCJ12,
+	author    = {Maik Merten and
+	             Falk Howar and
+	             Bernhard Steffen and
+	             Sofia Cassel and
+	             Bengt Jonsson},
+	editor    = {Cormac Flanagan and
+	             Barbara K{\"{o}}nig},
+	title     = {Demonstrating Learning of Register Automata},
+	booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
+	             - 18th International Conference, {TACAS} 2012, Held as Part of the
+	             European Joint Conferences on Theory and Practice of Software, {ETAPS}
+	             2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {7214},
+	pages     = {466--471},
+	publisher = {Springer},
+	year      = {2012},
+	url       = {https://doi.org/10.1007/978-3-642-28756-5\_32},
+	doi       = {10.1007/978-3-642-28756-5\_32},
+	timestamp = {Tue, 26 Jun 2018 14:11:56 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/tacas/MertenHSCJ12},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{DBLP:journals/tcs/MontanariS14,
 	author    = {Ugo Montanari and
 	             Matteo Sammartino},
@@ -1093,6 +1579,30 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DBLP:conf/tacas/MertenSHM11,
+	author    = {Maik Merten and
+	             Bernhard Steffen and
+	             Falk Howar and
+	             Tiziana Margaria},
+	editor    = {Parosh Aziz Abdulla and
+	             K. Rustan M. Leino},
+	title     = {Next Generation {LearnLib}},
+	booktitle = {Tools and Algorithms for the Construction and Analysis of Systems
+	             - 17th International Conference, {TACAS} 2011, Held as Part of the
+	             Joint European Conferences on Theory and Practice of Software, {ETAPS}
+	             2011, Saarbr{\"{u}}cken, Germany, March 26-April 3, 2011. Proceedings},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {6605},
+	pages     = {220--223},
+	publisher = {Springer},
+	year      = {2011},
+	url       = {https://doi.org/10.1007/978-3-642-19835-9\_18},
+	doi       = {10.1007/978-3-642-19835-9\_18},
+	timestamp = {Tue, 26 Jun 2018 14:11:57 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/tacas/MertenSHM11},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @proceedings{DBLP:conf/tacas/2008,
 	editor    = {C. R. Ramakrishnan and
 	             Jakob Rehof},
@@ -1183,6 +1693,49 @@
 	year={2013}
 }
 
+@thesis{Ploeger05,
+	title     = {Analysis of concurrent state machines in embedded copier software},
+	author    = {Bas Ploeger},
+	year      = {2005},
+	school    = {Master's thesis, Eindhoven University of Technology}
+}
+
+@article{DBLP:journals/sttt/RaffeltMSM09,
+	author    = {Harald Raffelt and
+	             Maik Merten and
+	             Bernhard Steffen and
+	             Tiziana Margaria},
+	title     = {Dynamic testing via automata learning},
+	journal   = {{STTT}},
+	volume    = {11},
+	number    = {4},
+	pages     = {307--324},
+	year      = {2009},
+	url       = {https://doi.org/10.1007/s10009-009-0120-7},
+	doi       = {10.1007/s10009-009-0120-7},
+	timestamp = {Thu, 18 May 2017 09:53:11 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/sttt/RaffeltMSM09},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@article{DBLP:journals/sttt/RaffeltSBM09,
+	author    = {Harald Raffelt and
+	             Bernhard Steffen and
+	             Therese Berg and
+	             Tiziana Margaria},
+	title     = {{LearnLib}: a framework for extrapolating behavioral models},
+	journal   = {{STTT}},
+	volume    = {11},
+	number    = {5},
+	pages     = {393--407},
+	year      = {2009},
+	url       = {https://doi.org/10.1007/s10009-009-0111-8},
+	doi       = {10.1007/s10009-009-0111-8},
+	timestamp = {Thu, 18 May 2017 09:53:11 +0200},
+	biburl    = {https://dblp.org/rec/bib/journals/sttt/RaffeltSBM09},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{DBLP:journals/iandc/RivestS93,
 	author    = {Ronald L. Rivest and
 	             Robert E. Schapire},
@@ -1246,6 +1799,20 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@book{DBLP:books/daglib/SelicGW94,
+	author    = {Bran Selic and
+	             Garth Gullekson and
+	             Paul T. Ward},
+	title     = {Real-time object-oriented modeling},
+	series    = {Wiley professional computing},
+	publisher = {Wiley},
+	year      = {1994},
+	isbn      = {978-0-471-59917-3},
+	timestamp = {Fri, 29 Apr 2011 18:24:07 +0200},
+	biburl    = {https://dblp.org/rec/bib/books/daglib/0078907},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @article{DBLP:journals/entcs/Shinwell06,
 	author    = {Mark R. Shinwell},
 	title     = {Fresh {O'Caml}: Nominal Abstract Syntax for the Masses},
@@ -1261,6 +1828,67 @@
 	bibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
+@inproceedings{DBLP:conf/icgi/SmetsersVVV14,
+	author    = {Rick Smetsers and
+	             Michele Volpato and
+	             Frits W. Vaandrager and
+	             Sicco Verwer},
+	editor    = {Alexander Clark and
+	             Makoto Kanazawa and
+	             Ryo Yoshinaka},
+	title     = {Bigger is Not Always Better: on the Quality of Hypotheses in Active
+	             Automata Learning},
+	booktitle = {Proceedings of the 12th International Conference on Grammatical Inference,
+	             {ICGI} 2014, Kyoto, Japan, September 17-19, 2014.},
+	series    = {{JMLR} Workshop and Conference Proceedings},
+	volume    = {34},
+	pages     = {167--181},
+	publisher = {JMLR.org},
+	year      = {2014},
+	url       = {http://jmlr.org/proceedings/papers/v34/smetsers14a.html},
+	timestamp = {Wed, 29 Mar 2017 16:45:26 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/icgi/SmetsersVVV14},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@inproceedings{DBLP:conf/sfm/SteffenHM11,
+	author    = {Bernhard Steffen and
+	             Falk Howar and
+	             Maik Merten},
+	title     = {Introduction to Active Automata Learning from a Practical Perspective},
+	booktitle = {Formal Methods for Eternal Networked Software Systems - 11th International
+	             School on Formal Methods for the Design of Computer, Communication
+	             and Software Systems, {SFM} 2011, Bertinoro, Italy, June 13-18, 2011.
+	             Advanced Lectures},
+	pages     = {256--296},
+	year      = {2011},
+	crossref  = {DBLP:conf/sfm/2011},
+	url       = {https://doi.org/10.1007/978-3-642-21455-4\_8},
+	doi       = {10.1007/978-3-642-21455-4\_8},
+	timestamp = {Wed, 25 Jul 2018 16:50:31 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/sfm/SteffenHM11},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
+@proceedings{DBLP:conf/sfm/2011,
+	editor    = {Marco Bernardo and
+	             Val{\'{e}}rie Issarny},
+	title     = {Formal Methods for Eternal Networked Software Systems - 11th International
+	             School on Formal Methods for the Design of Computer, Communication
+	             and Software Systems, {SFM} 2011, Bertinoro, Italy, June 13-18, 2011.
+	             Advanced Lectures},
+	series    = {Lecture Notes in Computer Science},
+	volume    = {6659},
+	publisher = {Springer},
+	year      = {2011},
+	url       = {https://doi.org/10.1007/978-3-642-21455-4},
+	doi       = {10.1007/978-3-642-21455-4},
+	isbn      = {978-3-642-21454-7},
+	timestamp = {Wed, 25 Jul 2018 16:50:31 +0200},
+	biburl    = {https://dblp.org/rec/bib/conf/sfm/2011},
+	bibsource = {dblp computer science bibliography, https://dblp.org}
+}
+
 @inproceedings{DBLP:conf/icst/TapplerAB17,
 	author    = {Martin Tappler and
 	             Bernhard K. Aichernig and

content/applying-automata-learning.tex

@@ -27,7 +27,7 @@ To the best of our knowledge, this is the first paper in which active automata l
 Once they have high-level models of the behaviour of software components, software engineers can construct better software in less time.
 A key problem in practice, however, is the construction of models for existing software components, for which no or only limited documentation is available.
 
-The construction of models from observations of component behaviour can be performed using regular inference (aka automata learning) techniques \citep[Ang87,Hig10,conf/sfm/SteffenHM11].
+The construction of models from observations of component behaviour can be performed using regular inference (aka automata learning) techniques \citep[DBLP:journals/iandc/Angluin87, Higuera10, DBLP:conf/sfm/SteffenHM11].
 The most efficient such techniques use the set-up of \emph{active learning,} illustrated in \in{Figure}[fig:learning], in which a \quotation{learner} has the task to learn a model of a system by actively asking questions to a \quotation{teacher}.
 
 \startplacefigure
@@ -47,10 +47,10 @@ Based on such a counterexample, the learner may then construct an improved hypot
 Hence, the task of the learner is to collect data by interacting with the teacher and to formulate hypotheses, and the task of the MBT tool is to establish the validity of these hypotheses.
 It is important to note that it may occur that an SUT passes the test for an hypothesis, even though this hypothesis is not valid.
 
-Triggered by various theoretical and practical results, see e.g. the work by \citet[BergGJLRS05,Leucker06,RSBM09,ThesisFides,CasselHJMS15,MertenHSCJ12,HowarSJC12], there is a fast-growing interest in automata learning technology.
+Triggered by various theoretical and practical results, see e.g. the work by \citet[DBLP:conf/fase/BergGJLRS05, DBLP:conf/fmco/Leucker06, DBLP:journals/sttt/RaffeltSBM09, Aarts14, DBLP:journals/jlp/CasselHJMS15, DBLP:conf/tacas/MertenHSCJ12, DBLP:conf/vmcai/HowarSJC12], there is a fast-growing interest in automata learning technology.
-In recent years, automata learning has been applied successfully, e.g., to regression testing of telecommunication systems \citep[HNS03], checking conformance of communication protocols to a reference implementation \citep[BRP14], finding bugs in Windows and Linux implementations of TCP \citep[FJV14], analysis of botnet command and control protocols \citep[ChocSS10], and integration testing \citep[LGS:forte06,GLPS:fates08].
+In recent years, automata learning has been applied successfully, e.g., to regression testing of telecommunication systems \citep[DBLP:conf/cav/HungarNS03], checking conformance of communication protocols to a reference implementation \citep[DBLP:journals/ml/AartsKTVV14], finding bugs in Windows and Linux implementations of TCP \citep[DBLP:conf/fmics/Fiterau-BrosteanJV14], analysis of botnet command and control protocols \citep[DBLP:conf/ccs/ChocSS10], and integration testing \citep[DBLP:conf/forte/LiGS06, DBLP:conf/pts/GrozLPS08].
 
-In this paper, we explore whether LearnLib \citep[RSBM09], a state-of-the-art automata learning tool, is able to learn a model of the Engine Status Manager (ESM), a piece of control software that is used in many printers and copiers of Oc\'{e}.
+In this paper, we explore whether LearnLib \citep[DBLP:journals/sttt/RaffeltSBM09], a state-of-the-art automata learning tool, is able to learn a model of the Engine Status Manager (ESM), a piece of control software that is used in many printers and copiers of Oc\'{e}.
 Software components like the ESM can be found in many embedded systems in one form or another.
 Being able to retrieve models of such components automatically is potentially very useful.
 For instance, if the software is fixed or enriched with new functionality, one may use a learned model for regression testing.
@@ -61,20 +61,20 @@ The ESM software is actually well documented, and an extensive test suite exists
 The ESM, which has been implemented using Rational Rose Real-Time (RRRT), is stable and has been in use for 10 years.
 Due to these characteristics, the ESM is an excellent benchmark for assessing the performance of automata learning tools in this area.
 The ESM has also been studied in other research projects:
-\citet[Plo:05] modelled the ESM and other related managers and verified properties based on the official specifications of the ESM, and \citet[conf/mompes/GraafD07]
+\citet[Ploeger05] modelled the ESM and other related managers and verified properties based on the official specifications of the ESM, and \citet[DBLP:conf/mompes/GraafD07]
 have checked the consistency of the behavioural specifications defined in the ESM against the RRRT definitions.
 
 Learning a model of the ESM turned out to be more complicated than expected.
 The top level UML/RRRT statechart from which the software is generated only has 16 states.
 However, each of these states contains nested states, and in total there are 70 states that do not have further nested states.
 Moreover, the \cpp{} code contained in the actions of the transitions also creates some complexity, and this explains why the minimal Mealy machine that models the ESM has 3.410 states.
-LearnLib has been used to learn models with tens of thousands of states by \citet[RaMeSM2009], and therefore we expected that it would be easy to learn a model for the ESM.
+LearnLib has been used to learn models with tens of thousands of states by \citet[DBLP:journals/sttt/RaffeltMSM09], and therefore we expected that it would be easy to learn a model for the ESM.
 However, finding counterexamples for incorrect hypotheses turned out to be challenging due to the large number of 77 inputs.
-The test algorithms implemented in LearnLib, such as random testing, the W-method by \citet[Ch78,vasilevskii1973failure] and the Wp-method by \citet[FBKAG91], failed to deliver counterexamples within an acceptable time.
+The test algorithms implemented in LearnLib, such as random testing, the W-method by \citet[DBLP:journals/tse/Chow78, Vasilevskii73] and the Wp-method by \citet[DBLP:journals/tse/FujiwaraBKAG91], failed to deliver counterexamples within an acceptable time.
-Automata learning techniques have been successfully applied to case studies in which the total number of input symbols is much larger, but in these cases it was possible to reduce the number of inputs to a small number ($< 10$) using abstraction techniques \cite{AJUV15,HoStMe2011}.
+Automata learning techniques have been successfully applied to case studies in which the total number of input symbols is much larger, but in these cases it was possible to reduce the number of inputs to a small number ($< 10$) using abstraction techniques \citep[DBLP:journals/fmsd/AartsJUV15, DBLP:conf/vmcai/HowarSM11].
 In the case of ESM, use of abstraction techniques only allowed us to reduce the original 156 concrete actions to 77 abstract actions.
 
-We therefore implemented and extension of the algorithm of \citet[LYa94] for computing an adaptive distinguishing sequence.
+We therefore implemented and extension of the algorithm of \citet[DBLP:journals/tc/LeeY94] for computing an adaptive distinguishing sequence.
 Even when an adaptive distinguishing sequence does not exist, Lee \& Yannakakis' algorithm produces an adaptive sequence that \quotation{almost} identifies states.
 In combination with a standard algorithm for computing separating sequences for pairs of states, we managed to verify states with on average 3 test queries and to learn a model of the ESM with 77 inputs and 3.410 states.
 We also constructed a model directly from the ESM software and established equivalence with the learned model.
@@ -83,7 +83,7 @@ Preliminary evidence suggests that our adaptation of Lee \& Yannakakis' algorith
 
 During recent years most researchers working on active automata learning focused their efforts on efficient algorithms and tools for the construction of hypothesis models.
 Our work shows that if we want to further scale automata learning to industrial applications, we also need better algorithms for finding counterexamples for incorrect hypotheses.
-Following \citet[BergGJLRS05], our work shows that the context of automata learning provides both new challenges and new opportunities for the application of testing algorithms.
+Following \citet[DBLP:conf/fase/BergGJLRS05], our work shows that the context of automata learning provides both new challenges and new opportunities for the application of testing algorithms.
 All the models for the ESM case study together with the learning and testing statistics are available at \todo{http://www.mbsd.cs.ru.nl/publications/papers/fvaan/ESM/}, as a benchmark for both the automata learning and testing communities.
 \todo{Link naar nieuwe benchmark site}
 
@@ -180,8 +180,8 @@ Messages can be sent to these ports using the action code of the transition.
 The transitions between the states, actions and guards are defined in \cpp{} code.
 From the state diagram, \cpp{} source files are generated.
 
-The RRRT language and semantics is based on UML \citep[OMGUML2] and ROOM \citep[ROOM94].
+The RRRT language and semantics is based on UML \citep[OMGUML2] and ROOM \citep[DBLP:books/daglib/SelicGW94].
-One important concept used in RRRT is the run-to-completion execution model \citep[EJW02].
+One important concept used in RRRT is the run-to-completion execution model \citep[DBLP:journals/re/EshuisJW02].
 This means that when a received message is processed, the execution cannot be interrupted by other arriving messages.
 These messages are placed in a queue to be processed later.
 
@@ -228,7 +228,7 @@ The possibility to transition from any state to the sleep or defect state also c
   [title={Learning the ESM},
    reference=sec:learning]
 
-In order to learn a model of the ESM, we connected it to LearnLib by \citet[conf/tacas/MertenSHM11], a state-of-the-art tool for learning Mealy machines developed at the University of Dortmund.
+In order to learn a model of the ESM, we connected it to LearnLib by \citet[DBLP:conf/tacas/MertenSHM11], a state-of-the-art tool for learning Mealy machines developed at the University of Dortmund.
 A \emph{Mealy machine} is a tuple $M = (I, O, Q, q_0, \delta, \lambda)$, where
 \startitemize
 \item $I$ is a finite set of input symbols,
@@ -269,7 +269,7 @@ Currently, LearnLib cannot handle inputs with parameters; therefore, we introduc
 Based on domain knowledge and discussions with the Oc\'{e} engineers, we could group some of these inputs together and reduce the total number of inputs.
 When learning the ESM using one function, 83 concrete inputs are grouped into four abstract inputs.
 When using two functions, 126 concrete inputs can be grouped.
-When an abstract input needs to be sent to the ESM, one concrete input of the represented group is randomly selected, as in the approach of \citet[AJUV15].
+When an abstract input needs to be sent to the ESM, one concrete input of the represented group is randomly selected, as in the approach of \citet[DBLP:journals/fmsd/AartsJUV15].
 This is a valid abstraction because all the inputs in the group have exactly the same behavior in any state of the ESM.
 This has been verified by doing code inspection.
 No other abstractions were found during the research.
@@ -313,8 +313,8 @@ An average test query takes around 1 ms, so it would take about 7 years to execu
   [title={Augmented DS-method.},
    reference=sec:randomPrefix]
 
-In order to reduce the number of tests, \citet[Ch78] and
+In order to reduce the number of tests, \citet[DBLP:journals/tse/Chow78] and
-\citet[vasilevskii1973failure] pioneered the so called W-method.
+\citet[Vasilevskii73] pioneered the so called W-method.
 In their framework a test query consists of a prefix $p$ bringing the SUT to a specific state, a (random) middle part $m$ and a suffix $s$ assuring that the SUT is in the appropriate state.
 This results in a test suite of the form $P I^{\leq k} W$, where $P$ is a set of (shortest) access sequences, $I^{\leq k}$ the set of all sequences of length at most $k$, and $W$ is a characterization set.
 Classically, this characterization set is constructed by taking the set of all (pairwise) separating sequences.
@@ -323,14 +323,14 @@ By increasing $k$ we can check additional states.
 
 We tried using the W-method as implemented by LearnLib to find counterexamples.
 The generated test suite, however, was still too big in our learning context.
-\citet[FBKAG91] observed that it is possible to let the set $W$ depend on the state the SUT is supposed to be.
+\citet[DBLP:journals/tse/FujiwaraBKAG91] observed that it is possible to let the set $W$ depend on the state the SUT is supposed to be.
 This allows us to only take a subset of $W$ which is relevant for a specific state.
 This slightly reduces the test suite without losing the power of the full test suite.
 This method is known as the Wp-method.
 More importantly, this observation allows for generalizations where we can carefully pick the suffixes.
 
 In the presence of an (adaptive) distinguishing sequence one can take $W$ to be a single suffix, greatly reducing the test suite.
-\citet[LYa94] describe an algorithm (which we will refer to as the LY algorithm) to efficiently construct this sequence, if it exists.
+\citet[DBLP:journals/tc/LeeY94] describe an algorithm (which we will refer to as the LY algorithm) to efficiently construct this sequence, if it exists.
 In our case, unfortunately, most hypotheses did not enjoy existence of an adaptive distinguishing sequence.
 In these cases the incomplete result from the LY algorithm still contained a lot of information which we augmented by pairwise separating sequences.
 
@@ -411,12 +411,12 @@ As mentioned already, the ESM has been implemented using Rational Rose RealTime
 Thus a statechart representation of the ESM is available.
 However, we have not been able to find a tool that translates RRRT models to Mealy machines, allowing us to compare the RRRT-based model of the ESM with the learned model.
 We considered several formalisms and tools that were proposed in the literature to flatten statecharts to state machines.
-The first one was a tool for hierarchical timed automata (HTA) \citep[david_02_formal].
+The first one was a tool for hierarchical timed automata (HTA) by \citet[DBLP:conf/fase/DavidMY02].
 However, we found it hard to translate the output of this tool, a network of Uppaal timed automata, to a Mealy machine that could be compared to the learned model.
-The second tool that we considered has been developed by \citet[conf/fmco/HansenKLMPS10].
+The second tool that we considered has been developed by \citet[DBLP:conf/fmco/HansenKLMPS10].
 This tool misses some essential features, for example the ability to assign new values to state variables on transitions.
 Finally, we considered a formalism called object-oriented action systems
-(OOAS) \citep[conf/fmco/KrennSA09], but no tools to use this could be found.
+(OOAS) by \citet[DBLP:conf/fmco/KrennSA09], but no tools to use this could be found.
 
 In the end we decided to implement the required model transformations ourselves.
 \in{Figure}[fig:formats] displays the different formats for representing models that we used and the transformations between those formats.
@@ -427,16 +427,16 @@ In the end we decided to implement the required model transformations ourselves.
 \externalfigure[formats.pdf][width=0.7\textwidth]
 \stopplacefigure
 
-We used the bisimulation checker of CADP \citep[conf/tacas/GaravelLMS11] to check the equivalence of labelled transition system models in {\tt .aut} format.
+We used the bisimulation checker of CADP \citep[DBLP:conf/tacas/GaravelLMS11] to check the equivalence of labelled transition system models in {\tt .aut} format.
 The Mealy machine models learned by LearnLib are represented as {\tt .dot} files.
 A small script converts these Mealy machines to labelled transition systems in {\tt .aut} format.
-We used the Uppaal \citep[conf/qest/BehrmannDLHPYH06] tool as an editor for defining extended finite state machines (EFSM), represented as {\tt .xml} files.
+We used the Uppaal \citep[DBLP:conf/qest/BehrmannDLHPYH06] tool as an editor for defining extended finite state machines (EFSM), represented as {\tt .xml} files.
 A script developed in the ITALIA project (\todo{http://www.italia.cs.ru.nl/}) converts these EFSM models to LOTOS, and then CADP takes care of the conversion from LOTOS to the {\tt .aut} format.
 
 The Uppaal syntax is not sufficiently expressive to directly encode the RRRT definition of the ESM, since this definition makes heavy use of UML \citep[OMGUML2] concepts such as state hierarchy and transitions from composite states, concepts which are not present in Uppaal.
 Using Uppaal would force us to duplicate many transitions and states.
 
-We decided to manually create an intermediate hierarchical EFSM (HEFSM) model using the UML drawing tool PapyrusUML \citep[lanusse2009papyrus].
+We decided to manually create an intermediate hierarchical EFSM (HEFSM) model using the UML drawing tool PapyrusUML \citep[LanusseTEMGTSDT09].
 The HEFSM model closely resembles the RRRT UML model, but many elements used in UML state machines are left out because they are not needed for modeling the ESM and complicate the transformation process.
 
 
@@ -555,7 +555,7 @@ This function takes a variable name and evaluates to the value of this variable
 \startsubsection
   [title={Results}]
 
-\in{Figure}[fig:esra-model] shows a visualization of the learned model that was generated using Gephi \citep[conf/icwsm/BastianHJ09].
+\in{Figure}[fig:esra-model] shows a visualization of the learned model that was generated using Gephi \citep[DBLP:conf/icwsm/BastianHJ09].
 States are coloured according to the strongly connected components.
 The number of transitions between two states is represented by the thickness of the edge.
 The large number of states (3.410) and transitions (262.570) makes it hard to visualize this model.
@@ -575,7 +575,7 @@ This phase is performed only once and thus only transitions from the initialisat
 During the construction of the RRRT-based model, the ESM code was thoroughly inspected.
 This resulted in the discovery of missing behaviour in one transition of the ESM code.
 An Oc\'{e} software engineer confirmed that this behavior is a (minor) bug, which will be fixed.
-We have verified the equivalence of the learned model and the RRRT-based model by using CADP \citep[conf/tacas/GaravelLMS11].
+We have verified the equivalence of the learned model and the RRRT-based model by using CADP \citep[DBLP:conf/tacas/GaravelLMS11].
 
 
 \stopsubsection
@@ -584,20 +584,20 @@ We have verified the equivalence of the learned model and the RRRT-based model b
   [title={Conclusions and Future Work},
    reference=sec:future]
 
-Using an extension of algorithm by \citet[LYa94] for adaptive distinguishing sequences, we succeeded to learn a Mealy machine model of a piece of widely used industrial control software.
+Using an extension of algorithm by \citet[DBLP:journals/tc/LeeY94] for adaptive distinguishing sequences, we succeeded to learn a Mealy machine model of a piece of widely used industrial control software.
 Our extension of Lee \& Yannakakis' algorithm is rather obvious, but nevertheless it appears to be new.
 Preliminary evidence suggests that it outperforms existing conformance testing algorithms.
 We are currently performing experiments in which we compare the new algorithm with other test algorithms on a number of realistic benchmarks.
 
 There are several possibilities for extending the ESM case study.
 To begin with, one could try to learn a model of the ESM with more than one function.
-Another interesting possibility would be to learn models of the EHM, ACM and other managers connected to the ESM. Using these models some of the properties discussed by \citet[Plo:05] could be verified at a more detailed level.
+Another interesting possibility would be to learn models of the EHM, ACM and other managers connected to the ESM. Using these models some of the properties discussed by \citet[Ploeger05] could be verified at a more detailed level.
 We expect that the combination of LearnLib with the extended Lee \& Yannakakis algorithm can be applied to learn models of many other software components.
 
 In the specific case study described in this article, we know that our learning algorithm has succeeded to learn the correct model, since we established equivalence with a reference model that was constructed independently from the RRRT model of the ESM software.
 In the absence of a reference model, we can never guarantee that the actual system behaviour conforms to a learned model.
 In order to deal with this problem, it is important to define metrics that quantify the difference (or distance) between a hypothesis and a correct model of the SUT, and to develop test generation algorithms that guarantee an upper bound on this difference.
-Preliminary work in this area is reported by \citet[SVVV14].
+Preliminary work in this area is reported by \citet[DBLP:conf/icgi/SmetsersVVV14].
 
 
 \stopsection