TOrPEDO: Witnessing Model Correctness with Topological Proofs
| العنوان: | TOrPEDO: Witnessing Model Correctness with Topological Proofs |
|---|---|
| المؤلفون: | Anna Bernasconi, Alessandro Maria Rizzi, Claudio Menghi, Paola Spoletini |
| المصدر: | info:eu-repo/grantAgreement/EC/H2020/694277 Formal Aspects of Computing |
| سنة النشر: | 2021 |
| مصطلحات موضوعية: | Model checking, Correctness, Computer science, 02 engineering and technology, Topology, Mathematical proof, Unsatisfiable Core, Theoretical Computer Science, Model Checking, 03 medical and health sciences, Development (topology), Satisfiability modulo theories, Unsatisfiable core, 0202 electrical engineering, electronic engineering, information engineering, Temporal logic, Topological proofs, Topological Proofs, Theorem proving, 030304 developmental biology, Computer science [C05] [Engineering, computing & technology], 0303 health sciences, Theorem Proving, Iterative Design, Iterative design, 020207 software engineering, Sciences informatiques [C05] [Ingénierie, informatique & technologie], Theory of computation, Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni, Software |
| الوصف: | 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 ( ≈ 60%) than their respective initial models effectively supporting designers in creating model revisions. In a significant number of cases ( ≈ 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. |
| اللغة: | English |
| URL الوصول: | https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b123daa31ad074fb1d1303c633c090a9 http://orbilu.uni.lu/handle/10993/47825 |
| Rights: | OPEN |
| رقم الانضمام: | edsair.doi.dedup.....b123daa31ad074fb1d1303c633c090a9 |
| قاعدة البيانات: | OpenAIRE |
كن أول من يترك تعليقا!