Specification Quality Metrics Based on Mutation and Inductive Incremental Model Checking - Archive ouverte HAL Access content directly
Book Sections Year : 2020

Specification Quality Metrics Based on Mutation and Inductive Incremental Model Checking

(1, 2, 3) , (4, 3) , (4, 3)
1
2
3
4

Abstract

When using formal verification on Simulink or SCADE models , an important question about their certification is how well the specified properties cover the entire model. A method using unsatisfiable cores and inductive model checking called IVC (Inductive Validity Cores) has been recently proposed within modern SMT-based model checkers such as JKind. The IVC algorithm determines a minimal set of model elements necessary to establish a proof and gives back the traceability to the design elements (lines of code) necessary for the proof. These metrics are interesting but are rather coarse grain for certification purposes. In this paper, we propose to use mutation combined with incremental inductive model checking to give more precision and quality to the trace-ability process and look inside the lines of code. Our algorithm, based on the result of IVC, mutates the source code to determine which parts inside a line of code have an impact on the properties (killed mutants) and which parts have no impact on the properties (survived mutants). Furthermore , using the incremental feature present in modern SMT-solvers, we observe that mutation can scale up to industrial models. We demonstrate the metrics first on a simple example, then on a complex industrial program and on the JKind benchmark.
Fichier principal
Vignette du fichier
Specification Quality Metrics Based on Mutation and Inductive Incremental Model Checking.pdf (762.02 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-02956436 , version 1 (02-10-2020)

Identifiers

Cite

Vassil Todorov, Safouan Taha, Frédéric Boulanger. Specification Quality Metrics Based on Mutation and Inductive Incremental Model Checking. NASA Formal Methods - 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11-15, 2020, Proceedings, pp.187-203, 2020, ⟨10.1007/978-3-030-55754-6_11⟩. ⟨hal-02956436⟩
51 View
104 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More