Model checking has reached a maturity level that allows its techniques to be applied to the verification of industrial systems. Several algorithms and methods have been proposed to increase its effectiveness to tackle models of increasing complexity. In this chapter we present an application of Parallel Satisfiability Solving to the verification of embedded control systems. The adopted toolchain is part of the Formal Specs Verifier framework for the formal verification of Simulink/Stateflow models. The experiments we performed show that the use of a parallel satisfiability solver allows for an average speedup of an order of magnitude or more on industrial strength models.

An application of parallel satisfiability solving to the verification of complex embedded systems / Ferrante, Orlando; Ferrari, Alberto; Sofronis, Christos; Mangeruca, Leonardo; Benvenuti, Luca. - STAMPA. - (2018), pp. 617-632. [10.1007/978-3-319-63516-3_16].

An application of parallel satisfiability solving to the verification of complex embedded systems

Benvenuti, Luca
2018

Abstract

Model checking has reached a maturity level that allows its techniques to be applied to the verification of industrial systems. Several algorithms and methods have been proposed to increase its effectiveness to tackle models of increasing complexity. In this chapter we present an application of Parallel Satisfiability Solving to the verification of embedded control systems. The adopted toolchain is part of the Formal Specs Verifier framework for the formal verification of Simulink/Stateflow models. The experiments we performed show that the use of a parallel satisfiability solver allows for an average speedup of an order of magnitude or more on industrial strength models.
2018
Handbook of parallel constraint reasoning
978-3-319-63515-6
978-3-319-63516-3
model checking; embedded systems; parallel satisfiability
02 Pubblicazione su volume::02a Capitolo o Articolo
An application of parallel satisfiability solving to the verification of complex embedded systems / Ferrante, Orlando; Ferrari, Alberto; Sofronis, Christos; Mangeruca, Leonardo; Benvenuti, Luca. - STAMPA. - (2018), pp. 617-632. [10.1007/978-3-319-63516-3_16].
File allegati a questo prodotto
File Dimensione Formato  
Ferrante_An-application_2018.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 790.7 kB
Formato Adobe PDF
790.7 kB Adobe PDF   Contatta l'autore
Ferrante_Frontespizio-indice_2018.pdf

solo gestori archivio

Tipologia: Versione editoriale (versione pubblicata con il layout dell'editore)
Licenza: Tutti i diritti riservati (All rights reserved)
Dimensione 761.9 kB
Formato Adobe PDF
761.9 kB Adobe PDF   Contatta l'autore

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/11573/1113161
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? ND
social impact