Active Learning of Abstract System Models from Traces using Model Checking [Extended]

TL;DR

This paper introduces an active learning method for creating finite state automata abstractions of system implementations from execution traces, using model checking to iteratively refine the models until they accurately represent system behaviors.

Contribution

It presents a novel active model-learning approach that integrates model checking to refine automata based on execution traces, improving abstraction accuracy.

Findings

Successfully reverse-engineered Simulink Stateflow models from C implementations.

Automated iterative refinement improves model completeness.

Method effectively captures system behaviors in automata.

Abstract

We present a new active model-learning approach to generating abstractions of a system implementation, as finite state automata (FSAs), from execution traces. Given an implementation and a set of observable system variables, the generated automata admit all system behaviours over the given variables and provide useful insight in the form of invariants that hold on the implementation. To achieve this, the proposed approach uses a pluggable model learning component that can generate an FSA from a given set of traces. Conditions that encode a completeness hypothesis are then extracted from the FSA under construction and used to evaluate its degree of completeness by checking their truth value against the system using software model checking. This generates new traces that express any missing behaviours. The new trace data is used to iteratively refine the abstraction, until all system behaviours are admitted by the learned abstraction. To evaluate the approach, we reverse-engineer a set of publicly available Simulink Stateflow models from their C implementations.