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

Vedere questo file PDF e questo file TGZ.

Date degli appelli

Appello	Data	Ora	Aula	Note	Scadenza
1	16/01/2025	09:00-11:00			12/01/2025 ore 23:59:59
2	30/01/2025	09:00-11:00			26/01/2025 ore 23:59:59
3	13/02/2025	09:00-11:00	Turing A1.1		09/02/2025 ore 23:59:59
4	06/2025
5	06/2025
6	07/2025
7	09/2025
straord	11/2025

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	26/09/2024	slides	Introduzione al testing, alla validazione ed alla verifica di sistemi software	Slides 1-73
	27/09/2024		ANNULLATA
2	03/10/2024	slides modelli Murphi	Il model checker Murphi: linguaggio di input e uso	Lezione 1: slides 73-fine. Lezione 2: Slides 1-end
3	04/10/2024	slides	Il model checker Murphi: algoritmo di verifica (parte 1)	Slides 1-33
4	10/10/2024	Vedere slides lezione 3	Il model checker Murphi: algoritmo di verifica (parte 2)	Slides 34-75
5	11/10/2024	slides	Il model checker Murphi: algoritmo di verifica (parte 3). Proprietà di safety e liveness. La logica temporale LTL (parte 1)	Lezione 3: Slides 76-fine. Lezione 5: Slides 1-14
6	17/10/2024	slides	La logica temporale LTL (parte 2) e CTL. Algoritmi per il CTL Model Checking	Lezione 5: Slides 15-fine. Lezione 6: Slides 1-4
7	18/10/2024	slides	Algoritmi per il Model Checking di formule CTL ed LTL. SPIN e Promela (parte 1)	Lezione 6: Slides 5-fine. Lezione 7: Slides 1-8
8	24/10/2024	Vedere slides lezione 7	SPIN e Promela (parte 2)	Slides 9-45
9	25/10/2024	Vedere slides lezione 8; modelli SPIN	SPIN e Promela (parte 3)	Slides 46-fine
10	31/10/2024	slides	NuSMV (parte 1: gli OBDD)	Slides 1-38
11	07/11/2024	Vedere slides lezione 10	NuSMV (parte 2: linguaggio di input)	Slides 39-78
12	08/11/2024	modelli e script per BMC slides	NuSMV (parte 3: algoritmi). Bounded Model Checking	Lezione 10: Slides 79-fine. Lezione 12: Slides 1-fine
13	14/11/2024		Presentazione progetto
14	15/11/2024	slides slides	Introduzione al Testing. Modelli Finiti (parte 1)	Slides 1-fine e 1-12
15	21/11/2024	Vedere slides lezione 14	Modelli Finiti (parte 2)	Slides 13-fine
16	22/11/2024	slides examples	Testing: Metodologie (parte 1: Category-Partition Testing)	Slides 1-39
17	28/11/2024	Vedere lezione 16	Testing: Metodologie (parte 2: Catalog-Based e Pairwise Combination Testing)	Slides 40-66
18	29/11/2024	Vedere slides lezione 16	Testing: Metodologie (parte 3: Structural Testing e Data Flow Testing)	Slides 67-106
19	05/12/2024	Vedere slides lezione 16	Testing: Metodologie (parte 4: Model-Based Testing)	Slides 107-150
20	06/12/2024	Vedere slides lezione 16	Testing: Metodologie (parte 5: Testing di Software Orientato agli Oggetti)	Slides 151-194
21	12/12/2024	Vedere slides lezione 16	Testing: Metodologie (parte 6: Scaffolding)	Slides 195-220
22	13/12/2024	slides	Integration, System, Acceptance e Regression Testing	Slides 221-fine e 1-fine
23	19/12/2024		Revisione progetti studenti
24	20/12/2024		Revisione progetti studenti

Orario delle lezioni

Giorno	Dalle	Alle	Aula
Giovedì	09:30	11:30	A.0.6
Venerdì	09:30	11:30	A.0.6

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