AbstractModel 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 , 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, 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 . The new
version of relies on a novel procedure to extract
topological proofs, which has so far represented the bottleneck of
performances. We implemented our procedure within 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 converts the LTL formulae into an
SMT instance and reuses an existing SMT solver (e.g., Microsoft
) to compute an unsatisfiable core. Then, the
unsatisfiable core returned by the SMT solver is automatically
processed to generate the topological proof. We evaluated by
assessing (i) how does the size of the proofs generated by
compares to the size of the models being analyzed; and (ii) how
frequently the use of the topological proof returned by
avoids re-executing the model checker. Our results show that
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 enable assessing
the property satisfaction without re-running the model checker. We
evaluated our new version of 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
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 are useful to support the development of
alternative design choices of (small) model instances in applied
domains.
Using a bounded model checker for test generation: How to kill two birds with one SMT solver
