print · source · login   

Tomte Tool

Description

Tomte is a tool that fully automatically constructs abstractions for automata learning. Usually, a component implementing the learning algorithm (the learner) is directly conncected 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.


Figure 1: Architecture of the learning framework

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 shrinked Nils Holgersson into a gnome and (after numerous adventures) changed him back to his normal size again.

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. All models we used in our experiments can be found in the .zip file in the Download section. If you want to learn your own model, please study the Making Your Own SUT section.

Download

The Tomte tool: tomte-0.1.zip
Platforms supported:  Windows, Linux and Mac OS X
For  other releases look here.

Requirements

Equivalence checking

With Tomte we can learn a model. However to verify what we have learned is really equivalent to the SUT we use the  the CADP toolset. Note: this toolset is not required for learning.

Usage

Step 1 : learn model Run the 'tomte_learn_model' command with the model you want to learn. When running without arguments it wil show you the models available :

 > tomte_learn_model 
 tomte_learn_model: error: too few arguments 
 usage: tomte_learn_model [-h] model 
 available models : 
 - ABP_Receiver3
 - FWGC2 
 - Login_XMPP_2
 - SIP2_1param 
 - Channel_Frame 
 - Repdigit_Palindrome_Checker4_Complete2
 - BiometricPassport
 - ABP-output

An example run :

 > tomte_learn_model BiometricPassport
 ...

Notes:

  • The 'BiometricPassport' model is fetched from the subfolder  'models'
  • Results are saved in the folder : 'results/BiometricPassport/'
  • In Windows you can also drag and drop model files on tomte_learn_model.bat

Step 2: check equivalence learned model with teacher model

For equivalence checking the CADP tool set is needed.

Only the lotos subfolder in the results folder is needed. If you are learning the model on a machine where the CADP toolset is not installed. Then only the learned lotos/ subfolder needs to be copied to the machine with the CADP toolset installed to check equivalence.

In this lotos/ results folder a bash script can be found with which you can do equivalence checking. The only requirement for this script to run is to set the path to the installed CADP toolset in the $CADP environment variable. For example :

 > export CADP=/vol/cadp/ 

Now you can do equivalence checking as follows :

 > cd tomte-0.1/results/BiometricPassport/lotos/ 
 > ./compare_lotos_models.sh BiometricPassport 
 ... 
 TRUE or FALSE with a trace 

As shown above the equivalence will print TRUE in case of equivalence and else FALSE with the trace showing the difference. Also different equivalences can be checked with the CADP toolset. The equivalence to be used can be given as the first argument to 'compare_lotos_models.sh'. When giving the '-h' option to this script it will output its usage description with the listing of all equivalence methods available. The default is 'strong'.

 > ./compare_lotos_models.sh -h 
 usage: compare_lotos_models.sh [eq_method]
  eq_method is one of the values:  
  strong,trace,weaktrace,branching,observational,safety,taustar 
  eq_method is by default : 'strong' 
 for more info see : http://www.inrialpes.fr/vasy/cadp/man/bisimulator.html 

Making Your Own SUT

We employ the UPPAAL GUI to specify SUTs. However, the syntax we use is slightly different from the syntax defined by the UPPAAL developers. We support modelling of locations and transitions, where

  • the name of every input event has to start with an 'I'. Similarly, every output event has to start with an 'O'. We do not allow synchronizations. So, every event name does not need to end with a '?' or '!', but with a list of parameter values in parentheses, or empty parentheses in case of no parameters, 
  • every transition can have a guard. We allow tests for equality (==) or inequality (!=) of parameter values, where different tests can be concatenated via '&&' or '||'. At the moment we only allow comparison of Integer values, and
  • every transition can have zero or more update statements to update the state variables, e.g. by storing parameter values. Every statement has to end with a semicolon.

Currently, Tomte can learn SUTs that may only remember the last and first occurrence of a parameter. We are not able yet to learn timed systems. Figure 2 shows an example model of the alternating bit protocol receiver that conforms to our syntax.

alternating bit protocol receiver
Figure 2: Example model of the alternating bit protocol receiver

In addition to modelling the system, we require a number of declarations (added in the 'Declarations' section in UPPAAL), which are

  • the constants that appear in the system,
  • the range of parameter values (min_value and max_value),
  • the range used for bisimulation checking (lts_min_value and lts_max_value). This range is needed when the learned Extended Finite State Machine (EFSM) is transformed into a LOTOS specification by means of the CADPtool set,
  • an enumeration of all state variables in the system, and
  • an enumeration of all events in the system.

For the alternating bit protocol receiver model shown above, the declarations are as follows:

 constants = 0,1;
 min_value = 0;
 max_value = 40;

 lts_min_value = 0;
 lts_max_value = 10;

 int vd;
 int vb;
 int expectedBit = 0;

 void IFrame(int d, int b) {
 }

 void IPleaseAck() {
 }

 void OOut(int vd) {
 }

 void OAck(int vb) {
 }

 void ONOK() {
 }

Finally, copy your file to the subfolder 'models'.

Contact

Feel free to email us on any topic concerning Tomte: