Radboud University Nijmegen (THE NETHERLANDS)
CADP (Construction and Analysis of Distributed Processes)
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.
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.
Fides Aarts, Harco Kuppens, Jan Tretmans, Frits Vaandrager, and
"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
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
Tel: +31 24 365 2216
Fax: +31 24 365 2525
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|