The tool consists of 3 main modules; analyzer, translator, and
instrumentor.
The analyzer module contains
our computation slicing and predicate detection algorithms. Given
an execution trace and a predicate (specification) in RCTL+, first the
computation slice with respect to the predicate is computed, then if
the initial state of the execution trace is contained in the
computation slice , the predicate is satisfied.
The translator module enables comparison
with other formal verification tools. Since we are working with
distributed programs which exhibit a lot of parallelism and
independency, partial order reduction techniques can take advantage of
these properties of distributed programs. The SPIN model checker
contains implementation of partial order reduction techniques.
Also, translation from traces to SMV is supported.
The instrumentation module inserts code
at the appropriate places in the program to be monitored. The
instrumented program is such that it outputs the values of variables
relevant to the predicate in question and keeps a vector clock that is
updated for each internal, send and receive event according to the
Fidge/Mattern algorithm. We use the vector clock to obtain a partial
order representation of traces.
|
