print · login   

Tomte Tool

Tomte is a tool that fully automatically constructs abstractions for automata learning. Usually, a component implementing the learning algorithm (the learner) is directly connected to the SUT (the teacher). By observing how the SUT responds to queries sent by the learner, a model of the behavior of the SUT can be constructed. This is not enough for learning models of realistic software components which, due to the presence of program variables and data parameters in messages, typically have much larger state spaces.

This inspired us to build the Tomte tool, which is placed in between the SUT and the learner, and transforms the large set of actions of the SUT into a small set of abstract actions that can be handled by the learner, see Figure 1. This means the inference is performed on a small alphabet and once the learning is done the abstract model is combined with the abstraction to construct a concrete version of the SUT. This gave us the idea for the name of the tool. Tomte is the creature that shrank Nils Holgersson into a gnome and (after numerous adventures) changed him back to his normal size again.


Figure 1: Architecture of the learning framework

We use LearnLib as our basic learning tool and therefore the abstraction of the SUT may not exhibit any nondeterminism: if it does then LearnLib crashes and we have to refine the abstraction. This is exactly what is implemented in the Tomte tool. As learner also other inference algorithms can be used as long as they detect nondeterministic behavior.

Using Tomte we have succeeded to learn - fully automatically - models of several realistic software components, including the biometric passport and the SIP protocol. We also support simulating an SUT from a state machine model. All models we used in our experiments can be found in the .zip file in the Downloads page. If you want to simulate your own model, please study the Making SUT? page. Note that we can only learn a restricted class of extended finite state machines (EFSM), i.e. Scalarset Mealy machines. For details on the restrictions, please study the Making SUT page and our paper "Automata Learning Through Counterexample-Guided Abstraction Refinement" [CEGAR12].

For questions, feedback or technical support for this website you can contact h.kuppens@cs.ru.nl.