Skip to Main content Skip to Navigation
Book sections

Specification Quality Metrics Based on Mutation and Inductive Incremental Model Checking

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.
Complete list of metadatas

Cited literature [25 references]  Display  Hide  Download
Contributor : Vassil Todorov <>
Submitted on : Friday, October 2, 2020 - 5:32:55 PM
Last modification on : Wednesday, October 14, 2020 - 4:21:57 AM


Specification Quality Metrics ...
Files produced by the author(s)



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⟩



Record views


Files downloads