Verifica automatica di sistemi (2017/2018)

Codice insegnamento
4S003252
Docente
Andrea Masini
Coordinatore
Andrea Masini
crediti
6
Settore disciplinare
INF/01 - INFORMATICA
Lingua di erogazione
Italiano
Periodo
II sem. dal 1-mar-2018 al 15-giu-2018.

Orario lezioni

Vai all'orario delle lezioni

Obiettivi formativi

Scopo di questo corso è introdurre le tecniche di model checking basate sulla logica temporale per la verifica di sistemi concorrenti.
Le tecniche di model checking sono le più utilizzate per verificare proprietà di sistemi concorrenti a stati finiti, dove l'attenzione è sulle proprietà di safety, liveness and fairness.
Alla fine del corso gli studenti avranno gli strumenti per affrontare ed applicare a casi reali le più moderne tecniche di verifica automatica di sistemi concorrenti a stati finiti

Programma

Verifica dei sistemi:
l’approccio basato sul model checking
Sistemi di modellazione concorrenti:
sistemi di transizione,
parallelismo e comunicazione,
esplosione degli stati
Proprietà del tempo lineare:
safety e invarianti,
liveness,
fairness
Linear Temporal Logic:
sintassi,
semantica,
fairness,
model checking
Computation Tree Logic:
sintassi,
semantica,
espressività di CTL vs LTL,
fairness,
model checking simbolico
CTL *
Equivalenza e astrazione:
bisimulazione,
bisimulazione e equivalenza in CTL *

Testi di riferimento
Autore Titolo Casa editrice Anno ISBN Note
Christel Baier and Joost-Pieter Katoen Principles of Model Checking MIT press 2008

Modalità d'esame

Esame scritto

Statistiche per i requisiti di trasparenza (Attuazione Art. 2 del D.M. 31/10/2007, n. 544)

I dati relativi all'AA 2017/2018 non sono ancora disponibili