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.
>