Tomte: Bridging the Gap between Active Learning and Real-World Systems

Fides Aarts

Promotor: prof.dr. F.W. Vaandrager (RU)
Radboud Universiteit Nijmegen
Date: 27 October, 2014, 10:30

Summary

Humans often manage to learn the behavior of a device or computer program by just pressing buttons and observing the resulting behavior. Especially children are very good in doing this and know exactly how to use a game computer, iPod or microwave oven without ever consulting a manual. In such situations we construct a mental model of a state diagram: we determine in which global states a device can be and which state transitions and outputs occur in response to which input.

This doctoral thesis deals with the design of algorithms that allow computers to learn complex state diagrams by providing inputs and observing outputs. The state diagrams that can be learned by standard techniques have at most 30,000 states. In contrast, the state diagrams that govern the behavior of computing based systems (defined using dozens of state variables) typically have more than 10¹⁰⁰⁰ states. We have further developed the standard techniques and have constructed a tool set that allows us to learn – routinely and fully automatically – state diagrams.

Once they have high-level models of the behavior of software components, software engineers can construct better software in less time: behavioral models can be used to simulate a system and reason about it, they allow all stakeholders to participate in the development process and to communicate with each other, they can be used to generate and test implementations, and they facilitate reuse. A key problem in practice, however, is the construction of models for existing software components, for which no or only limited
documentation is available.

In Part 2 of this thesis, we describe how by means of a so-called mapper component the basic learning techniques can be enhanced. The main idea is to place a mapper in between the standard learning algorithm and the system we want to learn – also known as system under test (SUT). The learning algorithm determines the sequence of buttons or abstract actions (e.g. an action with two parameters to which the same value has to be assigned) to be executed. These are translated by the mapper to inputs for the SUT by selecting concrete values for the data parameters. The selection is dependent on the history of messages sent earlier, which is maintained by the mapper. The resulting output of the SUT is again translated back by the mapper by abstracting away from concrete output
parameter values. In this way it is possible to map a large set of concrete transitions of a real-world system to a small set of abstract transitions of the learned state diagram. In this part, the notion of a mapper and the corresponding operations of abstraction and concretization are formalized. Moreover, it is shown that this approach works by manually defining the mapper and connecting it to the real-world system. We succeeded in learning models of some realistic communication protocols (TCP, SIP, and the new biometric passport).

Part 3 presents how the manually constructed mappers of Part 2 can be generated fully automatically for a restricted class of systems, in which one can test for equality of data parameters, but no operations on data are allowed. By means of counterexample-guided abstraction refinement abstractions, i.e. equalities between data parameters can be derived. If during testing of a hypothesized model an input leads to a different output than predicted earlier, we have found a counterexample. If this counterexample contains a new abstraction, it is added automatically to solve the problem. Also the mapper has been adapted to detect itself which values of previously sent messages have to be memorized. By running ‘future’ messages, we can find out whether a value is important in the future.
We have implemented our algorithm in the Tomte tool and succeeded in learning models of several realistic software components, including the biometric passport and the SIP protocol fully automatically.

Part 4 demonstrates how diverse application areas of active learning can be. It is shown how active learning can be used to test whether an implementation conforms to a reference implementation, i.e. an implementation of the specification or standard of the system. Using a well-known industrial case study, the bounded retransmission protocol, and a unique combination of software tools for model construction (Uppaal), active learning (LearnLib, Tomte), model-based testing (JTorX, TorXakis) and verification (CADP, MRMC) we succeeded in learning models of and revealing errors in several implementations.