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 per la specifica e verifica di proprietà
quantitative di sistemi. Verranno quindi introdotti i principi del model-checking probabilistico e stocastico. Infine, verranno
presentate alcune tecniche avanzate per l'analisi quantitativa di sistemi complessi.
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.