Metodi Formali nell'Ingegneria del Software

Programma del corso

Parte I: Il ruolo dei Metodi Formali nell'Ingegneria del Software

• Storia dei Metodi Formali
  • I problemi affrontati mediante i Metodi Formali
• Metodi Formali e ciclo di vita del software
  • Applicabilità alle varie fasi
  • Potenzialità e limiti

Parte II: Fondamenti logici dei Metodi Formali

• Logica Proposizionale
  • Generalità sulla logica
  • Sintassi
  • Semantica
  • Aspetti computazionali
  • Complessità computazionale
  • Algoritmi
  • Programmi disponibili
  • Esercitazioni: uso di SATZ, ZCHAFF e WALKSAT
• Logica dei predicati del primo ordine
  • Sintassi
  • Semantica
  • Rappresentazione in logica di frasi in italiano
  • L'uso della logica per esprimere proprietà di programmi
  • Asserzioni su uno stato del programma
  • Precondizioni e postcondizioni di una funzione Aspetti computazionali
  • Indecidibilità
  • Algoritmi
  • Programmi disponibili
  • Esercitazioni: uso di OTTER e MACE
• Logica proposizionale temporale
  • Sintassi di LTL
  • Semantica di LTL
  • Aspetti computazionali
  • Complessità
  • Algoritmi
  • Programmi disponibili
  • Esercitazioni: uso di NUSMV

Parte III: I Metodi Formali nella fase di analisi

• Diagrammi delle classi UML
  • Sintassi dei diagrammi delle classi UML
  • Semantica dei diagrammi delle classi UML
  • Proprietà dei diagrammi delle classi UML
  • Verifica di proprietà tramite un dimostratore di teoremi
  • Verifica di proprietà tramite un validatore di modelli
  • Esercitazioni: uso di OTTER, MACE e ALLOY ANALYZER
• Diagrammi UML degli stati e delle transizioni
  • Sintassi dei diagrammi degli stati e delle transizioni UML
  • Semantica dei diagrammi degli stati e delle transizioni UML
  • Proprietà dei diagrammi degli stati e delle transizioni UML
  • Verifica tramite un validatore di modelli
  • Esercitazioni: uso di NUSMV

Parte IV: I Metodi Formali nella fase di verifica

• Dimostrazione di correttezza di un programma
  • Sintassi dei programmi procedurali
  • Semantica dei programmi procedurali
  • L'uso della logica del prim'ordine per esprimere proprietà di programmi
  • Precondizioni e postcondizioni di una funzione
  • Correttezza parziale e totale di una funzione
  • L'uso della logica temporale per esprimere proprietà di programmi
  • Aspetti computazionali
  • Esercitazioni: uso di NUSMV