Specification Quality Metrics Based on Mutation and Inductive Incremental Model Checking

Vassil Todorov (1, 2, 3) , Safouan Taha (4, 3) , Frédéric Boulanger (4, 3)

1 Groupe PSA - Centre Technique de Vélizy [Vélizy-Villacoublay]
2 Université Paris-Saclay
3 LRI - Laboratoire de Recherche en Informatique
4 CentraleSupélec

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.

Mots clés: Formal verification; Model-based mutation; Incremental inductive model checking; Model coverage; Symbolic model checking

Domaines: Théorie et langage formel [cs.FL]; Génie logiciel [cs.SE]; Modélisation et simulation

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⟩