TOrPEDO: witnessing model correctness with topological proofs
2021
Model design is not a linear, one-shot process. It proceeds through
refinements and revisions. To effectively support developers in
generating model refinements and revisions, it is desirable to have
some automated support to verify evolvable models. To address this
problem, we recently proposed to adopt topological proofs,
which are slices of the original model that witness property
satisfaction. We implemented TOrPEDO, a framework that provides
automated support for using topological proofs during model design.
Our results showed that topological proofs are significantly smaller
than the original models, and that, in most of the cases, they allow
the property to be re-verified by relying only on a simple syntactic
check. However, our results also show that the procedure that
computes topological proofs, which requires extracting unsatisfiable
cores of LTL formulae, is computationally expensive. For this
reason, TOrPEDO currently handles models with a small dimension. With
the intent of providing practical and efficient support for flexible
model design and wider adoption of our framework, in this paper, we
propose an enhanced—re-engineered—version of TOrPEDO. The new
version of TOrPEDO relies on a novel procedure to extract
topological proofs, which has so far represented the bottleneck of
TOrPEDO performances. We implemented our procedure within TOrPEDO by
considering Partial Kripke Structures (PKSs) and Linear-time
Temporal Logic (LTL): two widely used formalisms to express models
with uncertain parts and their properties. To extract topological
proofs, the new version of TOrPEDO converts the LTL formulae into an
SMT instance and reuses an existing SMT solver (e.g., Microsoft
Z3) to compute an unsatisfiable core. Then, the
unsatisfiable core returned by the SMT solver is automatically
processed to generate the topological proof. We evaluated TOrPEDO by
assessing (i) how does the size of the proofs generated by TOrPEDO
compares to the size of the models being analyzed; and (ii) how
frequently the use of the topological proof returned by TOrPEDO
avoids re-executing the model checker. Our results show that TOrPEDO
provides proofs that are smaller (
$$\approx
$$
60%) than their
respective initial models effectively supporting designers in
creating model revisions. In a significant number of cases (
$$\approx
$$
79%), the topological proofs returned by TOrPEDO enable assessing
the property satisfaction without re-running the model checker. We
evaluated our new version of TOrPEDO by assessing (i) how it compares
to the previous one; and (ii) how useful it is in supporting the
evaluation of alternative design choices of (small) model instances
in applied domains. The results show that the new version of TOrPEDO
is significantly more efficient than the previous one and can
compute topological proofs for models with less than 40 states
within two hours. The topological proofs and counterexamples
provided by TOrPEDO are useful to support the development of
alternative design choices of (small) model instances in applied
domains.
Keywords:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
83
References
0
Citations
NaN
KQI