This case study involves learning models of TCP implementations and using these models
to check for specifications based on the RFC 793 standard.
This work builds on the learning TCP case study. We extend the alphabet with high
level socket calls, so models obtained by learning describe how these calls affect the
implementation's behavior. This brings these models closer to the actual TCP
implementations, as we can now use them to simulate TCP interaction by connecting client
and server TCP models to a model of a network. Next we connect sinks to each model
(simulating applications) and we can begin the simulation.
We use the models obtained by learning, and the network assembly described earlier
to automatically verify specifications using the NuSMV model checker. The specifications
are based on the RFC standard 793, some of which ensure proper functionality of the
protocol. By this verification we were able to capture some inconsistencies in the model.
The SUT (System Under Test) comprises TCP client and server implementations for
Windows 8, FreeBSD and Linux operating systems. The client and server differ by the
socket interface they provide.
A client can:
* send and receive data * connect to a server * close the TCP connection with a server
A server can:
* send and receive data * listen for and accept an incoming client connection * close the TCP connection with a client * close the server socket, by which it accepts client connections
Both the client and the server, as TCP implementations, respond to TCP packets sent to
their respective address. (so packets are also included in their full actual interface)
In previous work on TCP, the mapper was a program defined in an imperative language.
(C, Java) This was sufficient, as we did not have to consider concretizing the abstract
models obtained by learning. For this work, we need to concretize the models in order to
connect them in a network assembly, as their abstract interfaces are not compatible.
Concretely, the input alphabet is not the same as the output alphabet, thus an output
of one model cannot by readily served as input for the other. Concretizing both components
turns their interfaces to concrete (actual values), which now allows them to be connected.
For the purpose of defining a mapper we developed a language .
From the unified mapper definition so called abstraction and concretization components
are automatically derived. These components provide the abstraction of the system
necessary during learning, as well as concretization needed for simulation.
Having a unique mapper definition ensures consistency between the two components.
We have obtained models of Windows 8, Linux (Ubuntu 14.04) and FreeBSD TCP client and server
implementations. Since the models are large state machines, particularly the server models,
we display only one here. You can find all models on our repository here.
Each experiment has a folder containing the dot file "learnedModel.dot", which is the model obtained by learning.
You can use graphviz (and xdot) to visualize the model.
We show here the model of a Windows 8 TCP Client.
