Nel corso verranno introdotte alcune metodologie, basate su metodi formali, per la specifica e verifica
di proprietà di sistemi complessi. Verranno presentate le Algebre di Processo quale strumento per la specifica
dei comportamenti di sistemi e verranno usate logiche modali e temporali per la verifica delle proprietà qualitative.
Successivamente, verranno introdotti i principali algoritmi di model-checking.
Oltre alle proprietà qualitative, nel corso verranno introdotti anche gli strumenti p
J. Rutten, M. Kwiatkowska, G. Norman, D. Parker
Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems
American Mathematical Society, 2004
Christel Baier and Joost-Pieter Katoen
Principles Of Model Checking
MIT Press, 2008
Obiettivi Formativi
Lo scopo di questo corso è quello di introdurre lo studente nelle principali tecniche di specifica e di verifica basate su metodi formali. Durante il corso verranno presentate tecniche e metodologie che consentono di specificare e verificare in modo automatico proprietà qualitative e quantitative di sistemi complessi. Lo studente, inoltre, verrà introdotto nell'uso di strumenti automatici di supporto alla specifica e verifica.
Prerequisiti
Basi di logica. Principi di programmazione. Principi di probabilità.
Metodi Didattici
Lezioni in aula.
Modalità di verifica apprendimento
Esame orale e progetto
Programma del corso
Algebre di Processo. Logiche modali lineari: LTL. Model-checking di LTL. Logiche modali branching: CTL e mu-calcolo. Model-checking di CTL: algoritmo globale e algoritmo locale. Model-checking di mu-calcolo.
Proprietà quantitative di sistemi. Sistemi stocastici a tempo discreto: DTMC, PCTL, algoritmi di model-checking. Sistemi stocastici a tempo continuo: CTMC, CSL, algoritmi di model-checking. Tecniche avanzate di model-checking quantitativo.