Model Checking: Teoria ed Applicazioni

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.