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.

Abstract

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.

Cite this Paper

BibTeX
@InProceedings{pmlr-v21-aarts12a, title = {Learning and Testing the Bounded Retransmission Protocol}, author = {Aarts, Fides and Kuppens, Harco and Tretmans, Jan and Vaandrager, Frits and Verwer, Sicco}, booktitle = {Proceedings of the Eleventh International Conference on Grammatical Inference}, pages = {4--18}, year = {2012}, editor = {Heinz, Jeffrey and Higuera, Colin and Oates, Tim}, volume = {21}, series = {Proceedings of Machine Learning Research}, address = {University of Maryland, College Park, MD, USA}, month = {05--08 Sep}, publisher = {PMLR}, pdf = {http://proceedings.mlr.press/v21/aarts12a/aarts12a.pdf}, url = {https://proceedings.mlr.press/v21/aarts12a.html}, abstract = {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.} }
Endnote
%0 Conference Paper %T Learning and Testing the Bounded Retransmission Protocol %A Fides Aarts %A Harco Kuppens %A Jan Tretmans %A Frits Vaandrager %A Sicco Verwer %B Proceedings of the Eleventh International Conference on Grammatical Inference %C Proceedings of Machine Learning Research %D 2012 %E Jeffrey Heinz %E Colin Higuera %E Tim Oates %F pmlr-v21-aarts12a %I PMLR %P 4--18 %U https://proceedings.mlr.press/v21/aarts12a.html %V 21 %X 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.
RIS
TY - CPAPER TI - Learning and Testing the Bounded Retransmission Protocol AU - Fides Aarts AU - Harco Kuppens AU - Jan Tretmans AU - Frits Vaandrager AU - Sicco Verwer BT - Proceedings of the Eleventh International Conference on Grammatical Inference DA - 2012/08/16 ED - Jeffrey Heinz ED - Colin Higuera ED - Tim Oates ID - pmlr-v21-aarts12a PB - PMLR DP - Proceedings of Machine Learning Research VL - 21 SP - 4 EP - 18 L1 - http://proceedings.mlr.press/v21/aarts12a/aarts12a.pdf UR - https://proceedings.mlr.press/v21/aarts12a.html AB - 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. ER -
APA
Aarts, F., Kuppens, H., Tretmans, J., Vaandrager, F. & Verwer, S.. (2012). Learning and Testing the Bounded Retransmission Protocol. Proceedings of the Eleventh International Conference on Grammatical Inference, in Proceedings of Machine Learning Research 21:4-18 Available from https://proceedings.mlr.press/v21/aarts12a.html.

Related Material