GO TO ENGLISH VERSION

ALTRI ANNI ACCADEMICI

Indice:

Informazioni sugli esami

Programma del corso

Libri di testo

Materiale sulle lezioni

Orario delle lezioni

Software per il corso

Informazioni sugli esami

Regole per gli esami

Vedere la lezione 1.

Testo del progetto

TBA

Date degli appelli

Appello	Data	Ora	Aula	Note	Scadenza
1	approx 01/2027
2	approx 02/2027
3	approx 02/2027
4	approx 06/2027
5	approx 07/2027
6	approx 07/2027
7	approx 09/2027
straord	approx 11/2027

Programma del corso

Introduzione alla verifica

• il problema della verifica
• testing, model checking ed altre metodologie

Metodologie di Model Checking per Sistemi a Stati Finiti

• modellazione in Murphi, SPIN e NuSMV
• logiche temporali CTL ed LTL
• algoritmi di model checking: teorico, esplicito, simbolico, bounded model checking

Metodologie di Testing

• principali tecniche: testing funzionale e strutturale
• il testing nel processo di sviluppo del software: unit, integration, regression e system testing
• uso di JUnit

Metodologie di Validazione

• acceptance testing

Libri di testo consigliati:

• Gerald Everett, Raymond McLeod Jr.: Software Testing: Testing Across the Entire Software Development Life Cycle, Wiley
• Una versione del libro è disponibile sul sistema bibliotecario di Ateneo
• Mauro Pezzé, Michal Young: Software Testing and Analysis: Process, Principles, and Techniques, Wiley
• Una versione del libro è disponibile qui
• Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, Roderick Bloem (Editors): Handbook of Model Checking, Springer
• Una versione del libro è disponibile qui
• Christel Baier, Joost-Pieter Katoen: Principles of Model Checking, MIT Press
• Una versione del libro è disponibile qui

Materiale sulle lezioni

N	Data	Materiale	Argomenti	Note
1	24/09/2026	slides	Introduzione al testing, alla validazione ed alla verifica di sistemi software	Slides 1-51
	25/09/2026		ANNULLATA
	01/10/2026		ANNULLATA
2	02/10/2026	slides modelli Murphi	Il model checker Murphi: linguaggio di input e uso	Lezione 1: slides 52-fine. Lezione 2: Slides 1-fine
3	08/10/2026	slides	Il model checker Murphi: algoritmo di verifica (parte 1)	Slides 1-37
4	09/10/2026	Vedere slides lezione 3	Il model checker Murphi: algoritmo di verifica (parte 2)	Slides 38-fine
5	15/10/2026	slides	Proprietà di safety e liveness. La logica temporale LTL	Slides 1-29
6	16/10/2026	slides	La logica temporale CTL. Algoritmi per il CTL Model Checking	Lezione 5: Slides 30-fine. Lezione 6: Slides 1-28
7	22/10/2026	slides	Algoritmi per il Model Checking di formule LTL. SPIN e Promela (parte 1)	Lezione 6: Slides 29-fine. Lezione 7: Slides 1-35
8	23/10/2026	Vedere slides lezione 7	SPIN e Promela (parte 2)	Slides 36-55
9	29/10/2026	slides	SPIN e Promela (parte 3). NuSMV (parte 1: gli OBDD)	Lezione 7: Slides 56-fine. Lezione 9: Slides 1-7
10	30/10/2026	Vedere slides lezione 9	NuSMV (parte 2: linguaggio di input)	Slides 8-56

Orario delle lezioni

Giorno	Dalle	Alle	Aula
Giovedì	08:30	10:30	A.0.6
Venerdì	09:30	11:30	A1.3

L'aula A1.3 si trova al primo piano dell'edificio Alan Turing.

L'aula A.0.6 si trova oltre la biblioteca al piano terra di Coppito 1 (edificio Renato Ricamo); attenzione: si raggiunge passando al di fuori dell'edificio stesso.

Software (gratis) per il corso

• CMurphi
• SPIN
• NuSMV
• JUnit