Hardware systems complexity has constantly increased in recent years. Guaranteeing their correctness is a must. Formal verification techniques, like model checking, now play a major role in industrial environments. Their efficiency in dealing with large sets of properties is crucial. This paper deals with property grouping, decomposition, and coverage in model checking. Property grouping is a valuable solution whenever several properties must be proven for a single model. As such sets may include "easy-to-prove" and/or "similar" properties, grouping can reduce overhead avoiding sub-tasks repetition. Property decomposition, following the divide-and-conquer paradigm, can be effective whenever a property turns out to be "hard-to-prove". Our contribution is a heuristic property manager, running on top of a multi-engine model checking portfolio, aiming at productivity optimization. We compare different clustering heuristics and we exploit decomposition strategies for property sub-setting. We also consider the problem of evaluating a coverage measure for properties, used to monitor the "advancement" of the verification task.

To Split or to Group: From Divide-and-Conquer to Sub-Task Sharing for Verifying Multiple Properties in Model Checking / Cabodi, Gianpiero; Camurati, Paolo Enrico; Loiacono, Carmelo; Palena, Marco; Pasini, Paolo; Patti, Denis; Quer, Stefano. - In: INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER. - ISSN 1433-2779. - 20:(2018), pp. 313-325. [10.1007/s10009-017-0451-8]

To Split or to Group: From Divide-and-Conquer to Sub-Task Sharing for Verifying Multiple Properties in Model Checking

CABODI, Gianpiero;CAMURATI, Paolo Enrico;LOIACONO, CARMELO;PALENA, MARCO;PASINI, PAOLO;PATTI, DENIS;QUER, Stefano
2018

Abstract

Hardware systems complexity has constantly increased in recent years. Guaranteeing their correctness is a must. Formal verification techniques, like model checking, now play a major role in industrial environments. Their efficiency in dealing with large sets of properties is crucial. This paper deals with property grouping, decomposition, and coverage in model checking. Property grouping is a valuable solution whenever several properties must be proven for a single model. As such sets may include "easy-to-prove" and/or "similar" properties, grouping can reduce overhead avoiding sub-tasks repetition. Property decomposition, following the divide-and-conquer paradigm, can be effective whenever a property turns out to be "hard-to-prove". Our contribution is a heuristic property manager, running on top of a multi-engine model checking portfolio, aiming at productivity optimization. We compare different clustering heuristics and we exploit decomposition strategies for property sub-setting. We also consider the problem of evaluating a coverage measure for properties, used to monitor the "advancement" of the verification task.
File in questo prodotto:
File Dimensione Formato  
Cabodi2018_Article_ToSplitOrToGroupFromDivide-and.pdf

non disponibili

Tipologia: 2a Post-print versione editoriale / Version of Record
Licenza: Non Pubblico - Accesso privato/ristretto
Dimensione 665.63 kB
Formato Adobe PDF
665.63 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/2665134