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 | |||

http://hdl.handle.net/10993/41633 | |||

Integrating Topological Proofs with Model Checking to Instrument Iterative Design | |

English | |

Menghi, Claudio [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >] | |

Rizzi, Alessandro Maria [Politecnico di Milano] | |

Bernasconi, Anna [Politecnico di Milano] | |

Apr-2020 | |

Proceedings of the 23rd International Conference on Fundamental Approaches to Software Engineering, FASE 2020 | |

53-74 | |

Yes | |

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. | |

http://hdl.handle.net/10993/41633 | |

H2020 ; 694277 - TUNE - Testing the Untestable: Model Testing of Complex Software-Intensive Systems |

File(s) associated to this reference | ||||||||||||||

| ||||||||||||||

All documents in ORBi^{lu} are protected by a user license.