The dataset contains source code and data relevant for the paper "Combining Model Learning and Model Checking to Analyze TCP Implementations".Paper url: https://link.springer.com/chapter/10.1007/978-3-319-41540-6_25PDF url: http://www.sws.cs.ru.nl/publications/papers/fvaan/FJV16/main.pdfRamon Janssen's Master's thesis url: http://www.ru.nl/publish/pages/769526/z_thesis_ramon_janssen.pdfIn this work, we use automata learning with abstraction to infer models of 3 TCP client and server implementations (Windows, Linux, FreeBSD). We then verify properties on these models using the NuSMV model checker. The dataset comprises the software components of our experimental setup apart from the actual implementations, some useful scripts and the learned models and associated experimental logs.In more concrete terms, the dataset contains:- the learner (setup) implementation - Java code for the setup built around LearnLib to perform learning with abstraction over sockets. Abstraction is provided by a mapper, described in a mapper language described in the Master's thesis.- the mapper library - Java code for loading mappers written in the mapper language and executing them in both directions (from abstract to concrete and from concrete to abstract)- the network adapter - crafts packets from strings or messages ("SYN(0,10)") and sends them to a TCP entity, receives packets and turns them back to strings- mappers - the mappers defined for the three operating systems learned- experimental data - Mealy Machine models for 6 TCP client/server implementations (BitVise, OpenSSH, DropBear) accompanied by other experimental data (statistics, input configuration ...)- model checking setup - project comprising bash scripts and Java libraries used to perform model checking on the learned models, model checking is mostly automatedWhat can be re-used:- the learner setup (connect to the learner through the mapper to a different system over sockets), note that there are some limitations of the mapper language- the mapper adapter, again note the limitations which fit the TCP case study but may not fit other case studies- the network adapter, can be adapted to learn other lower layer protocols or can be tweaked to include more information from packets in strings- model checking setup, this cannot really be reused outside of the TCP case study but it may serve as inspiration for one who wants to perform model checking of concretized abstract models (the mappers used to learn the models were also used to concretize them during model checking) or of interactions between two parties- beautifying Java library (if one wants to make complex .dot files more readable)Also, the dataset is suitable for one who wants to try out/expand learning for TCP. Learning and model checking can be done with minimal adaptation (perhaps slight changes in the mapper and adapting the model checking scripts).Paper Abstract: We combine model learning and model checking in a challenging case study involving Linux, Windows and FreeBSD implementations of TCP. We use model learning to infer models of different software components and then apply model checking to fully explore what may happen when these components (e.g. a Linux client and a Windows server) interact. Our analysis reveals several instances in which TCP implementations do not conform to their RFC specifications.