Oce Technologies B.V. and Radboud University Nijmegen (THE NETHERLANDS)
CADP (Construction and Analysis of Distributed Processes)
Embedded control software.
3410 states, 262570 transitions.
Automata Learning consists in constructing a model of the behaviour
of a software component from observations. In this paper, automata
learning, and in particular the state-of-the-art automata learning tool
LearnLib, is used to construct a behavioural model of the ESM (Engine
Status Manager), a piece of control software that is used in many
printers and copiers of Oce. The aim is, e.g., to use the learned
model for regression testing of future versions of the software.
To verify the correctness of the model learned automatically from the ESM using LearnLib, its equivalence was checked with a model that was generated directly from the code of the ESM itself. To this aim, a transformation was devised from the RRRT (Rational Rose RealTime) code of the ESM to an automaton in the .aut format. The learned automaton was also transformed into the .aut format and both automata were compared using a bisimulation checker of CADP.
This work shows that LearnLib is effective in learning a model of an
industrial software component. The use of CADP has allowed to verify
the equivalence between the learned model and the model derived from
the RRRT implementation.
Wouter Smeenk, Joshua Moerman, Frits Vaandrager, and David Jansen.
"Applying Automata Learning to Embedded Control Software."
In Proceedings of the 17th International Conference on Formal
Engineering Methods ICFEM'2015, LNCS volume 9407, pages 67-83.
Springer-Verlag, November 2015.
Available on-line at: http://sws.cs.ru.nl/publications/papers/fvaan/ESM/main.pdf
or from our FTP site in PDF or PostScript
Faculty of Science
Radboud University Nijmegen
P.O. Box 9010, 6500 GL
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|