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.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
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.