Learning and Testing the Bounded Retransmission Protocol


Fides Aarts, Harco Kuppens, Jan Tretmans, Frits Vaandrager, Sicco Verwer ;
Proceedings of the Eleventh International Conference on Grammatical Inference, PMLR 21:4-18, 2012.


Using a well-known industrial case study from the verification literature, the bounded retransmission protocol, we show how active learning can be used to establish the correctness of protocol implementation I relative to a given reference implementation R. Using active learning, we learn a model M_R of reference implementation R, which serves as input for a model based testing tool that checks conformance of implementation I to M_R. In addition, we also explore an alternative approach in which we learn a model M_I of implementation I, which is compared to model M_R using an equivalence checker. Our work uses a unique combination of software tools for model construction (Uppaal), active learning (LearnLib, Tomte), model-based testing (JTorX, TorXakis) and verification (CADP, MRMC). We show how these tools can be used for learning these models, analyzing the obtained results, and improving the learning performance.

Related Material