Database of Case Studies Achieved Using CADP

Applying Automata Learning to Embedded Control Software

Organisation: Oce Technologies B.V. and Radboud University Nijmegen (THE NETHERLANDS)

Method: Mealy machines

Tools used: LearnLib
CADP (Construction and Analysis of Distributed Processes)

Domain: Embedded control software.

Period: 2015

Size: 3410 states, 262570 transitions.

Description: 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.

Conclusions: 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.

Publications: [Smeenk-Moerman-Vaandrager-Jansen-15] 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:
or from our FTP site in PDF or PostScript
Frits Vaandrager
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:

Last modified: Tue Mar 15 12:30:41 2016.

Back to the CADP case studies page