FORMAL METHODS FOR SYSTEM VERIFICATION

Anno accademico
2023/2024 Programmi anni precedenti
Titolo corso in inglese
FORMAL METHODS FOR SYSTEM VERIFICATION
Codice insegnamento
CM0474 (AF:451549 AR:245280)
Lingua di insegnamento
Inglese
Modalità
In presenza
Crediti formativi universitari
6
Livello laurea
Laurea magistrale (DM270)
Settore scientifico disciplinare
INF/01
Periodo
I Semestre
Anno corso
1
Sede
VENEZIA
Spazio Moodle
Link allo spazio del corso
Il corso si propone di fornire le basi teoriche per l'utilizzo di strumenti formali di modellazione, analisi e verifica sia di software che di sistemi informatici complessi.
Il corso presenta i principali strumenti formali per specificare ed analizzare il comportamento di un sistema di processi che interagiscono fra di loro con particolare attenzione all'analisi delle prestazioni.
In particolare verrà introdotto un calcolo stocastico che consente di descrivere ed analizzare il comportamento dinamico di sistemi distribuiti e concorrenti.
Lo studente acquisirà conoscenze e competenze sugli aspetti fondamentali da considerare nella progettazione di software con requisiti di affidabilità e prestazioni.
In particolare, acquisirà conoscenze sui metodi formali per la verifica e la valutazione delle prestazioni di sistemi concorrenti e distribuiti.
Saprà inoltre utilizzare gli strumenti formali e le metodologie per la modellazione dei sistemi, così come le tecniche per la progettazione e l'analisi di software e sistemi che soddisfino determinati requisiti di affidabilità e prestazioni.

E' richiesta una conoscenza di base di matematica e del calcolo delle probabilità.
Verrà introdotta l'algebra dei processi, stocastica, detta PEPA (acronimo di: Performance Evaluation Process Algebra) e verranno presentate alcune tecniche di analisi delle prestazioni.
- Il linguaggio PEPA: sintassi e semantica.
- Distribuzione stazionaria.
- Metodi di aggegazione e relazioni di equivalenza.
- Forme prodotto.
- Applicazioni all'analisi delle prestazioni.
- J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996. http://www.dcs.ed.ac.uk/pepa/book.pdf
- Articoli forniti dal docente.
L'esame può essere svolto in due modi:
- svolgendo un progetto di modellazione e analisi di un semplice sistema informatico e sostenendo una prova orale sul progetto e sul programma del corso allo scopo di verificare le competenze e capacità dello studente nell'applicare le conoscenze apprese durante il corso
oppure
- svolgendo una prova scritta nelle date degli appelli. La prova scritta consiste in esercizi di modellazione e analisi di semplici sistemi informatici allo scopo di verificare le competenze e capacità dello studente nell'applicare le conoscenze apprese durante il corso.
scritto
Lezioni teoriche ed esercizi svolti alla lavagna.
Sostenibilità:

Insegnamento sostenibile
Dispense e materiali di approfondimento disponibili online; testi di riferimento in formato e-book
Forum virtuali
Piattaforme e-learning, moodle
Programma definitivo.
Data ultima modifica programma: 20/03/2023