Parallel verification of temporal properties using dynamic analysis

Verification methods can be classified according to two kinds of criteria: static or not - i.e. dynamic - and formal or not. This paper follows a work about verification of temporal properties using dynamic analysis. The approach proposes to transform an LTL property into a Büchi automaton and to run the automaton on an execution trace to be verified. Because traces are finite, the end of trace problem can be bypassed with computation of statistical information about the verified trace if and only if the property follows a predefined given pattern. For very big traces, this approach is well-adapted, but traces have to be sequentially verified. This paper proposes to parallelize the verification approach by splitting the execution trace and executing the Büchi automaton on each sub-trace separately analysable, which allows a significant time saving.