Modellazione di Sistemi Discreti: strutture di Kripke. Logiche Temporali con cui esprimere specifiche: CTL, LTL, CTL*. Verifica che un sistema soddisfa una specifica logica: il Problema del Model Checking, complessità computazionale e soluzioni classiche. Principali soluzioni al Model checking: - esplicito: automi di Buchi, computazione on-the-fly, riduzioni dello spazio degli stati (simmetria e ordine parziale) - simbolico: mu-calcolo e OBDD. Compositional Reasoning Software Model Checking Bounded Model Checking Probabilistic Model Checking

Il testo di riferimento è "Model Checking, Second Edition", di Edmund M. Clarke, Jr., Orna Grumberg, Daniel Kroening, Doron Peled and Helmut Veith, 2018 E' consigliato anche il libro "Handbook of Model Checking", Editors: Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R., 2018 Le slide ed il materiale dei docenti si trovano sul sito del corso: http://twiki.di.uniroma1.it/twiki/view/MFS/FormalMethodsInSoftwareDevelopment20192020

Utilizzo di Model Checkers per la verifica dei sistemi HW/SW: - Model checker espliciti: SPIN e Murphi - Model checker simbolico, bounded ed unbounded: NuSMV - Software model checkers: CBMC - Probabilistic model checkers: FHP-Murphi e PRISM Di ciascuna categoria di model checkers vengono presentati: - linguaggio di input - modello di esecuzione - logica per la specifica delle proprietà - tecniche di implementazione

Il testo di riferimento è "Model Checking, Second Edition", di Edmund M. Clarke, Jr., Orna Grumberg, Daniel Kroening, Doron Peled and Helmut Veith, 2018 E' consigliato anche il libro "Handbook of Model Checking", Editors: Clarke, E.M., Henzinger, Th.A., Veith, H., Bloem, R., 2018 Le slide ed il materiale dei docenti si trovano sul sito del corso: http://twiki.di.uniroma1.it/twiki/view/MFS/FormalMethodsInSoftwareDevelopment20192020