Reference : Integrating Topological Proofs with Model Checking to Instrument Iterative Design
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Security, Reliability and Trust
Integrating Topological Proofs with Model Checking to Instrument Iterative Design
Menghi, Claudio mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Rizzi, Alessandro Maria [Politecnico di Milano]
Bernasconi, Anna [Politecnico di Milano]
Proceedings of the 23rd International Conference on Fundamental Approaches to Software Engineering, FASE 2020
Fundamental Approaches to Software Engineering
from 25-04-2019 to 30-04-2019
[en] Topological Proofs ; Iterative Design ; Model Checking ; Theorem Proving ; Unsatisfiable Core
[en] System development is not a linear, one-shot process. It proceeds through refinements and revisions. To support assurance that the system satisfies its requirements, it is desirable that continuous verification can be performed after each refinement or revision step. To achieve practical adoption, formal verification must accommodate continuous verification efficiently and effectively. Model checking provides developers with information useful to improve their models only when a property is not satisfied, i.e., when a counterexample is returned. However, it is desirable to have some useful information also when a property is instead satisfied. To address this problem we propose TOrPEDO, an approach that supports verification in two complementary forms: model checking and proofs. While model checking is typically used to pinpoint model behaviors that violate requirements, proofs can instead explain why requirements are satisfied. In our work, we introduce a specific notion of proof, called Topological Proof. A topological proof produces a slice of the original model that justifies the property satisfaction. Because models can be incomplete, TOrPEDO supports reasoning on requirements satisfaction, violation, and possible satisfaction (in the case where satisfaction depends on unknown parts of the model). Evaluation is performed by checking how topological proofs support software development on 12 modeling scenarios and 15 different properties obtained from 3 examples from literature. Results show that: (i) topological proofs are ≈60% smaller than the original models; (ii) after a revision, in ≈78% of cases, the property can be re-verified by relying on a simple syntactic check.
H2020 ; 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems

File(s) associated to this reference

Fulltext file(s):

Open access
fase.pdfAuthor postprint612.73 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.