FORMAL METHODS FOR SYSTEM VERIFICATION

L'insegnamento è una delle attività formative di base del corso di studio: [CM90] Computer Science and Information Technology. L'obiettivo dell'insegnamento è quello di fornire le basi teoriche, logico-matematiche, per l'utilizzo di strumenti formali di modellazione, analisi e verifica sia di software che di sistemi informatici complessi. In particolare, l'insegnamento si propone di introdurre 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. Queste conoscenze sono quindi utilizzate per introdurre uno specifico 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. Più in dettaglio;

1. Conoscenza e comprensione
● Conoscere i metodi formali per la verifica del software
● Conoscere i metodi formali per l'analisi delle prestazioni di sistemi concorrenti e distribuiti
● Conoscere le basi della modellazione di sistemi dinamici

2. Capacità di applicare conoscenza e comprensione
● Saper utilizzare gli strumenti formali per l'analisi del software
● Saper utilizzare le metodologie per la modellazione di sistemi complessi
● Saper applicare le conoscenze di base alla definizione di un modello per l'analisi di un sistema informatico reale

3. Capacità di giudizio
● Saper scegliere la metodologia più adatta in base al sistema da analizzare,

4. Abilità comunicative
● Sapere descrivere i requisiti di affidabilità e prestazioni che si vogliono analizzare
● Sapere interagire con i pari e con il tutor, in modo critico e rispettoso, in presenza e sul forum

5. Capacità di apprendimento
● Saper prendere appunti e condividerli in forma collaborativa sulla piattaforma on-line
● Saper consultare criticamente i testi di riferimento e la bibliografia in essi contenuta.

E' richiesta una conoscenza di base di matematica e del calcolo delle probabilità. È inoltre necessaria la comprensione della lingua inglese scritta e orale in modo da potere comprendere il materiale messo a disposizione dalla docente.

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 sostenuto in due modi:
1) Una prova scritta con la possibilità di una prova orale integrativa, se ritenuto necessario dalla docente o su richiesta dello studente. La prova scritta consiste in domande aperte sugli argomenti del corso ed esercizi. L'orale viene svolto solo se la prova scritta è risultata sufficiente. In caso di esito negativo dell'orale, sarà necessario ripetere lo scritto.
2) Un progetto e una prova orale. La prova orale prevede la discussione del progetto e in domande sul programma del corso.

Descrizione della prova scritta:
La prova scritta ha l’obiettivo di valutare le competenze di problem solving dello studente, la conoscenza dei concetti fondamentali, e la capacità di risolvere esercizi e dimostrare teoremi. Consiste in esercizi a risposta aperta riguardanti i principali argomenti trattati nel corso. Durante la prova scritta non è consentito l'uso di appunti, libri o dispositivi elettronici.
La prova scritta può essere seguita da una prova orale, qualora la docente lo ritenga opportuno o lo studente desideri integrare l’esito. L’esame orale consiste in una discussione degli elaborati, una verifica delle capacità di problem solving e un accertamento delle conoscenze teoriche e delle competenze espressive. L'orale viene svolto solo se la prova scritta è risultata sufficiente. In caso di esito negativo dell'orale, sarà necessario ripetere lo scritto.

Nel caso in cui lo studente scelga l’opzione 2) la valutazione dell'esame terrà conto della qualità del progetto (30%), della qualità della relazione che lo descrive (20%), della capacità di esporre i concetti fondamentali della disciplina (50%).

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

Questo insegnamento tratta argomenti connessi alla macroarea "Città, infrastrutture e capitale sociale" e concorre alla realizzazione dei relativi obiettivi ONU dell'Agenda 2030 per lo Sviluppo Sostenibile