Model checking on inferred TCP-models
Ramon Janssen
Radboud University
Model checking is a powerful technique for finding errors in specifications and implementations. Models of separate systems can be easily composed into networks, and required properties can be checked automatically. But models are often handwritten, which makes it difficult to ensure that such models correspond with the behavior of the system they describe. We can solve this problem with automata learning, which yields models by directly interacting with the system, thereby learning its behavior.
We have used this approach to learn models of TCP clients and servers in an automated way. Normally, the number of possible values for parameters in TCP packets is too large for learning or model checking. By means of parameter abstraction we reduce this number for the sequence and acknowledgement numbers. This reduces the size of the model, so that the learning of these systems can be performed efficiently.
The resulting models are then imported into a model checker. By reversing the abstraction in the model checker, we check a model with concrete parameters, which behaves like the real-world system. By combining models of servers and clients of different operating systems, we verify that all outputs generated by the client are accepted by the server, and vice versa.
