Learning Concise Models from Long Execution Traces (trace2model)

Paper: https://arxiv.org/pdf/2001.05230.pdf
Github: https://github.com/natasha-jeppu/Trace2Model/tree/develop

Introduction

Motivation -- What can we learn from the traces

Hardware & Software are designed in different companies
->
People want to know the behaviors of software on specific hardware
->

Concise, human-readable models that express high-level hardware-software interactions can provide users with a better insight into the working of the system. This can, in turn, aid in design exploration, analysis, testing and veriﬁcation applications.

Example of a model (NFA) that may be learned from traces

This is a model described the slot-level operations of a USB.

Key insights -- Why this algorithm/model is good

Scalable -- by segmentation approach
Produce the abstract, concise model
Can form the transition-edge predicates that are not explicit in the trace.
Use SAT-based approach with program synthesis

Preliminaries

Terminology to define the traces

$X = {x_{1}, . . ., x_{k}}$ : variables
$X^{'} = {x_{1}^{'}, . . ., x_{k}^{'}}$ : primed variables variables (represents an update to the unprimed variable $x_{i}$ at the end of a discrete step.)
$D$ : domain $D$ , where the values of variables $X$ and $X^{'}$ settle
$v$ : valuation $X \to D$ (assign value to variable $x$ )
$v_{t}$ : observation. a valuation of the variables at time step $t$
$δ = v_{1}, v_{2}, . . ., v_{n}$ : trace. It's a trace with $n$ observations as a sequence of valuations.

The final NFA (Non-Deterministic Finite Automation) model

$M = (Q, q_{0}, Σ, F, δ)$

$M$ : NFA machine
$Q$ : finite set of states, and $q_{0} \in Q$ is the initial state.
$Σ$ : finite alphabet. A symbol $a \in Σ$ is $X \cup X^{'} \to D$ , i.e., a pair of observation of the system.
The symbol $a_{i}$ for $i = 1, . . ., n - 1$ is

a_{i} (x) = v_{i} (x),

a_{i} (x^{'}) = v_{i + 1} (x)

$F \subseteq Q$ is the set of accepting states.
$δ : Q \times Σ \to P (Q)$ : transition relation, define how one state goes to the next state.

The automation accepts a word $w = a_{1}, . . ., a_{p}$ over $Σ$ for $p < n$ if there exists a sequence of automaton states $q_{1}, . . ., q_{p + 1}$ such that

$q_{1} = q_{0}$
$q_{i + 1} \in δ (q_{i}, a_{i})$ for $i = 1, . . ., p .$ (there is transition relation can translate one state to the next state)

Algorithm

Generate Trace (is not included in the model)
->
Predicate Synthesizer
->
Construct the machine

Predicate Synthesizer

What to generate

Generate the synthesized function $n e x t (x)$ according to the trace data, a predicate is $x^{'} = n e x t (x)$ .

This paper is using Fastsynth and CVC4 to synthesize these predicate.

Notice that, the trace is feed into the Fastsynth and CVC4 by segments

So, the predicates are from the segments

Form the model (Generate the NFA)

The machine $M$ is essentially an array with each element is a tuple of $(q_{i}, p_{i}^{'}, q_{i}^{'})$
$M = {((q_{1}, p_{1}^{'}, q_{1}^{'}), (q_{2}, p_{2}^{'}, q_{2}^{'}), (q_{m}, p_{m}^{'}, q_{m}^{'}))}$

Divide the predicates we obtained before according to the sliding window with length $w$ .
Find the machine using CBMC to find the counterexample, the steps are:
1. Set the constraint be no such machine exists
2. Form the C program that uses the predicates from $P$ we obtained from step 2 to fit the machine $M$
3. Use CBMC to verify this formed machine.
  - If assertion holds, no such machine exists, we incremental the state size $N$
  - If assertion not hold, we can get the counterexample. We then need to verify if all transition sequences in $M$ belong to $P$ . If not, we need to add the constraints and form other C program.