Il model checking è una tecnica algoritmica per la verifica di proprietà temporali di sistemi dinamici, introdotto nella prima parte degli anni ’80. Le tecniche iniziali di model checking a stati finiti, basate sull’esplorazione esplicita dello spazio degli stati, sono state progressivamente sostituite, nel corso degli anni, da tecniche simboliche, ovvero basate su Diagrammi di Decisione Binaria (BDD), e sistemi per la soddisfacibilità proposizionale (SAT solvers). Ulteriori sviluppi nel model checking, orientati all’analisi di sistemi a stati infiniti, derivano dalla applicazione di tecniche per la soddisfacibilità modulo teorie (SMT). Si tratta di procedure di decisione per frammenti della logica del primo ordine, che possono essere viste come una integrazione di SAT con tecniche per la risoluzione di vincoli. Il model checking è applicato in molti ambiti a supporto della progettazione, debugging e certificazione di sistemi a stati finiti e infiniti. Obiettivo di questo lavoro è fornire una introduzione alla teoria del model checking, ed una panoramica delle sue applicazioni in vari ambiti della sicurezza.

Model Checking: Teoria ed Applicazioni / A. Cimatti, S. Ghilardi, S. Ranise (ANALITICA). - In: Le direzioni della ricerca logica in Italia 2 / [a cura di] H. Hosni, G. Lolli, C. Toffalori. - [s.l] : Edizioni ETS, 2018. - ISBN 9788846752987. - pp. 141-194

Model Checking: Teoria ed Applicazioni

S. Ghilardi;
2018

Abstract

Il model checking è una tecnica algoritmica per la verifica di proprietà temporali di sistemi dinamici, introdotto nella prima parte degli anni ’80. Le tecniche iniziali di model checking a stati finiti, basate sull’esplorazione esplicita dello spazio degli stati, sono state progressivamente sostituite, nel corso degli anni, da tecniche simboliche, ovvero basate su Diagrammi di Decisione Binaria (BDD), e sistemi per la soddisfacibilità proposizionale (SAT solvers). Ulteriori sviluppi nel model checking, orientati all’analisi di sistemi a stati infiniti, derivano dalla applicazione di tecniche per la soddisfacibilità modulo teorie (SMT). Si tratta di procedure di decisione per frammenti della logica del primo ordine, che possono essere viste come una integrazione di SAT con tecniche per la risoluzione di vincoli. Il model checking è applicato in molti ambiti a supporto della progettazione, debugging e certificazione di sistemi a stati finiti e infiniti. Obiettivo di questo lavoro è fornire una introduzione alla teoria del model checking, ed una panoramica delle sue applicazioni in vari ambiti della sicurezza.
Settore INF/01 - Informatica
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
main.pdf

accesso riservato

Tipologia: Pre-print (manoscritto inviato all'editore)
Dimensione 632.28 kB
Formato Adobe PDF
632.28 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

Caricamento 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: http://hdl.handle.net/2434/591317
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact