Verranno introdotte le tecniche basate su metodi formali per la specifica e verifica dei sistemi complessi. Le algebre di processo saranno utilizzate come strumento per la modellizzazione dei sistemi. Le logiche modali e temporali saranno usate per specificare le proprietà dei sistemi. Algoritmi di model-checking saranno quindi introdotti per verificare se i modelli considerati soddisfano o meno i requisiti. Nel corso sia le proprietà qualitative che quelle quantitative verranno considerate.
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.