METODI FORMALI DELL'INFORMATICA E LOGICA PER L'INFORMATICA - MODULO 2: METODI FORMALI


Docente: Marina Lenisa

OBIETTIVO DEL CORSO

L'obiettivo del modulo di Metodi Formali è quello di fornire allo studente strumenti rigorosi per la verifica formale di correttezza di programmi. In particolare, verra` illustrata la Logica di Hoare, basata su invarianti, per la verifica di programmi sequenziali, paralleli e distribuiti. 
Si discuteranno formalmente correttezza e terminazione di diversi algoritmi sequenziali classici. Mentre questioni come assenza di deadlock e fairness verranno affrontate formalmente per una serie di problemi paradigmatici di concorrenza, quali produttore-consumatore, trasmissione di dati.

PROGRAMMA

- Introduzione alla verifica formale della correttezza di programmi.
- Sintassi e semantica operazionale di programmi deterministici.
- Sistema di regole alla Hoare per la correttezza di programmi deterministici.
- Verifica formale di algoritmi sequenziali classici. Correttezza parziale e terminazione.
- Completezza dei sistemi di regole alla Hoare.
- Sintassi e Semantica Operazionale di programmi paralleli disgiunti.
- Riduzione del parallelismo disgiunto alla sequenzialita`.
- Verifica di programmi paralleli disgiunti.
- Verifica di programmi paralleli con variabili condivise: correttezza parziale.
- Correttezza Forte dei proof outline. Regola per il parallelismo e sua incompletezza. Regola per le variabili ausiliarie.
- Correttezza totale di programmi paralleli con variabili condivise.
- Programmi paralleli con variabili condivise. Comportamento non-composizionale delle componenti.
- Programmi paralleli con sincronizzazione: sintassi, semantica operazionale.
- Verifica di correttezza di programmi paralleli con sincronizzazione: correttezza parziale, terminazione, assenza di deadlock.
- Verifica di correttezza di esempi classici di programmi paralleli con sincronizzazione: produttore e consumatore, lettori e scrittori, implementazione e uso di semafori, etc.
- Programmi non-deterministici: sintassi, semantica operazionale, regole per la verifica di correttezza.
- Utilita` dei programmi non-deterministici. Traduzione di programmi paralleli in programmi non-deterministici.
- Introduzione alla programmazione distribuita. Programmi distribuiti: sintassi, semantica operazionale.
- Esempi classici: il problema della trasmissione nelle sue varianti (con e senza filtraggio di dati, con e senza messaggi di acknowledgment, etc).
- Traduzione di programmi distribuiti in programmi non-deterministici e relazioni tra le semantiche.
- Verifica: correttezza parziale, terminazione, assenza di deadlock.
- Fairness: studio della correttezza di programmi paralleli sotto l'ipotesi di schedulazione fair. La metodologia presentata si basa sull'implementazione di uno scheduler fair all'interno del programma stesso. Tale implementazione e` definita su un linguaggio esteso con assegnamento random. La prova di terminazione richiede l'utilizzo di funzioni di terminazione definite su strutture ben fondate che generalizzano i naturali.

Trasparenze di alcune lezioni:



- Introduzione alla verifica formale della correttezza di programmi.

- Sintassi e semantica operazionale di programmi deterministici.

- Asserzioni, formule per la correttezza, nozione di sostituzione di varaibiali in espressioni e asserzioni.

- Sistema di regole alla Hoare per la correttezza di programmi deterministici. Esempi.

- Esercizi. Completezza dei sistemi PD e TD.

- Verifica di programmi paralleli disgiunti

- Verifica di programmi paralleli con variabili condivise: correttezza parziale.

- Correttezza totale di programmi paralleli con variabili condivise.

- Programmi paralleli con variabili condivise: correttezza del programma FINDPOS. Programmi paralleli con sincronizzazione: sintassi, semantica operazionale.



BIBLIOGRAFIA:



- Trasparenze usate a lezione
- Apt K., de Boer F., Olderog E-R., "Verification of Sequential and Concurrent Programs", Springer, 3rd edition, 2009.



>