Jan 24, 2017: Marcus Gerhold: Passive Learning for Verification

January 24, 2017Passive Learning for Verification
Room: HB 2AMarcus Gerhold
12:30-13:30

Model-Based testing is a way to automate the testing process, aiming at the validation of real life reactive and embedded systems. Test cases are automatically generated, executed and evaluated based on a model.

One bottleneck of this work-flow is often where models come from. We present our current advances in inaugurating automata learning into this automated flow in two parts:

One approach is that of passive learning. The learning algorithm incorporates additional information, often in the form of log files, to facilitate the learning process. While general passive learning algorithms are NP-complete, we use probabilistic passive learning algorithms shown to run in polynomial time. Our goal is to reconstruct usage profiles from end users that may assist in test case selection.

In the second part of this talk we present the research idea of a supersized learn-based testing toolset. This learn-based testing toolset extends traditional active automata learning techniques with LTL requirements, and passive learning techniques to augment test case generation. The model checker guides the learner with counter examples towards parts of the state space that are relevant for disproving the LTL formula. The user profiles guide the learner towards parts of the state space that are actually relevant for the user of the system.

Our work is still work in progress.