Learning and Testing the Bounded Retransmission Protocol

Organisation:	Radboud University Nijmegen (THE NETHERLANDS)
Method:	Mealy machines
Tools used:	UPPAAL LearnLib, Tomte JTorX, TorXakis CADP (Construction and Analysis of Distributed Processes) MRMC
Domain:	Communication Protocols.
Period:	2012
Size:	n/a.
Description:	State machine models, such as Mealy machines, are suitable for specifying the behavior of software systems, by describing the way in which they react to different inputs, and when they produce which output. Unfortunately, the construction of finite state machine descriptions is often omitted during software development. An alternative to constructing these models manually, is to use software model synthesis (or system identication/learning, or process discovery/mining) tools in order to derive them automatically from data. This data typically consists of execution traces, i.e., sequences of operations, function calls, user interactions, or protocol primitives, which are produced by the system or its surrounding environment. Intuitively, software model synthesis tries to discover the logical structure (or model) underlying these sequences of events. This can be seen as a grammatical inference problem in which the events are modeled as the symbols of a language, and the goal is to find a model for this language. This work uses Mealy machine learning methods in order to establish the correctness of protocol implementations relative to a given reference implementation (which is assumed to be correct). Using a state machine synthesis tool, a state machine model MR of the reference implementation R is actively learned. Given another implementation I, two conformance approaches are considered. The first approach provides MR as input to a model based testing tool, which will use MR to generate test sequences and apply them to implementation I in order to establish its conformance to the learned model MR. The second approach uses the synthesis tool to learn a model MI of the other implementation I, and then uses an equivalence checker to check the behavioral equivalence of MR and MI. The fail verdicts and counterexamples provided by the two approaches can be fed to the synthesis tools in order to obtain more refined models of the two implementations R and I. The approach is illustrated on the bounded retransmission protocol (BRP), a data link protocol that was developed by Philips Research to support infrared communication between a remote control and a television. A unique combination of tools is used: UPPAAL serves as editor for extended finite state machines (EFSM); LearnLib serves for learning Mealy machines, subsequently converted to LTSs; CADP serves for equivalence checking of LTSs (using BISIMULATOR); JTorX and TorXAkis establish conformance of mutant implementations to the LTS model of the reference implementation; MRMC serves to compute the probability of reaching certain states in an implementation within a certain number of steps in a setting where inputs are generated randomly; and Tomte bridges the gap between the EFSMs used in software systems and the Mealy machines used by active learning tools. This learning and analysis approach was successfully applied to check conformance between a reference implementation of the BRP and six mutant implementations.
Conclusions:	The objective of this study was to combine active Mealy machine learning methods with model-based testing in order to quickly discover the behavioral differences between variations and the reference model. The approach adopted made use of several state-of-the-art tools from grammatical inference, software testing, and formal verification. It was shown how these tools can be used for learning models of the BRP, analyzing the obtained results, and improving the performance of the learning methods. This demonstrates how active learning can be used in an industrial setting by combining it with software verification and testing tools, and showing how these tools can also be used to analyze and improve the results of learning.
Publications:	[Aarts-Kuppens-Tretmans-et-al-12] Fides Aarts, Harco Kuppens, Jan Tretmans, Frits Vaandrager, and Sicco Verwer. "Learning and Testing the Bounded Retransmission Protocol". Journal of Machine Learning Research 21:4-18, 2012. Available on-line at: http://www.mbsd.cs.ru.nl/publications/papers/fvaan/BRP12/BRP.pdf or from the CADP Web site in PDF or PostScript [Aarts-Kuppens-Tretmans-Vaandrager-Verwer-14] Fides Aarts, Harco Kuppens, Jan Tretmans, Frits Vaandrager, and Sicco Verwer. "Improving Active Mealy Machine Learning for Protocol Conformance Testing". Machine Learning 96(1-2):189-224, July 2014. Available on-line at: http://link.springer.com/article/10.1007%2Fs10994-013-5405-0 or from the CADP Web site in PDF or PostScript
Contact:	Prof. dr. Frits W. Vaandrager Institute for Computing and Information Sciences Mailbox 47, Faculty of Science Radboud University Nijmegen Heijendaalseweg 135, Huygens Building 6525 AJ Nijmegen The Netherlands Tel: +31 24 365 2216 Fax: +31 24 365 2525 Email: F.Vaandrager@cs.ru.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page