Learning Concise Models from Long Execution Traces
This work addresses the need for efficient model extraction in system design and verification, though it appears incremental as it builds on existing program synthesis techniques.
The authors tackled the problem of automatically extracting abstract models from long execution traces of hardware/software systems, and they developed an algorithm that uses program synthesis and trace segmentation to generate concise automata models, demonstrating it on traces from sources like x86 QEMU and Real-Time Linux.
Abstract models of system-level behaviour have applications in design exploration, analysis, testing and verification. We describe a new algorithm for automatically extracting useful models, as automata, from execution traces of a HW/SW system driven by software exercising a use-case of interest. Our algorithm leverages modern program synthesis techniques to generate predicates on automaton edges, succinctly describing system behaviour. It employs trace segmentation to tackle complexity for long traces. We learn concise models capturing transaction-level, system-wide behaviour--experimentally demonstrating the approach using traces from a variety of sources, including the x86 QEMU virtual platform and the Real-Time Linux kernel.