Tomte-0.2

Related publications: [AKTVV12]

The Mapper

We used the Tomte tool [AHKOV12] to automatically construct a mapper for mutant 1. Through the use of counterexample-guided abstraction refinement, Tomte is able to learn models for a restricted class of extended finite state machines in which one can test for equality of data parameters, but no operations on data are allowed. Version 0.2 of Tomte requires that only the first and the last occurrence of parameters of actions is remembered. As a result, Tomte 0.2 can only learn models such as mutant 1, where each IREQ input overwrites previous occurrences of the message parameters. For the reference implementation and the other mutants we did not use a mapper component, but directly connected the learner to the SUT, i.e. the Java executable.

The Learned Model

Fig. 2: Learned model of mutant 1 using Tomte and a retransmission counter of 5. With CADP [GLMS11] we could show that the learned model is bisimilar to the SUT.    

We also learned correct models for the reference implementation and the other mutants. However, every model contains at least 100 states, which is not readable any more. Therefore, we decided to show only the model of mutant 1, which has 'only' 38 states due to the abstraction refinement techniques contained in Tomte.