Complex System Design

ORARIO DELLE LEZIONI:

- GIOVEDI' DALLE 16:00 ALLE 18:00

- VENERDI' DALLE 09:00 ALLE 13:00

Le lezioni del corso di Complex Systems Design riprenderanno il giorno 18 Ottobre 2018

Apprendere i concetti fondazionali e le tecniche di base per modellare e analizzare sistemi software. Acquisire consapevolezza dello stato dell'arte per ciò che concerne la progettazione rigorosa di software ed essere in grado di personalizzare e contestualizzare i metodi acquisiti. Applicare le tecniche proposte in contesti reali quali sistemi operativi, protocolli di comunicazione, linguaggi di programmazione concorrenti e orientati agli oggetti.

Analisi e verifica dei sistemi software complessi richiedono una progettazione rigorosa. Questo è particolarmente evidente per i cosiddetti sistemi “safety-critical”, in cui errori nel codice possono avere conseguenze disastrose (perdita di vite umane, finanziarie etc.). L'uso di tecniche rigorose applicate allo studio e allo sviluppo di sistemi software è quindi essenziale, non solo al fine di scongiurare errori catastrofici, ma anche per evitare una lievitazione dei costi legata alla loro correzione tardiva. Il testing è in grado di identificare problemi, ma non è generalmente sufficiente per garantire un livello di qualità soddisfacente. I metodi formali - come le Algebre di Processo, che forniscono un apparato formale per ragionare in modo composizionale sulla struttura ed il comportamento dinamico dei sistemi - offrono invece tecniche rigorose che vanno dalla descrizione dei requisiti attraverso notazioni formali fino a tecniche di verifica automatica del software. Questo corso mira a proporre agli studenti i concetti fondazionali delle Algebre di Processo senza perdere di vista le necessità pratiche e applicative dei programmatori e degli analisti di software. Tratterà le tecniche di base per descrivere forma e significato dei termini di processo e per ragionare su questi in modo rigoroso. Il contesto di studio scelto sarà il CCS, un ben noto linguaggio per sistemi reattivi, ed alcune delle sue estensioni più importanti. Sulla base di questi calcoli verranno discusse alcune nozione di equivalenza e tecniche di dimostrazione associate. Durante il corso verranno prese in considerazione anche calcoli CCS-like orientati all'analisi integrata della correttezza funzionale, delle performance e di aspetti di dipendenza dei sistemi software.

Contenuti: - Introduzione ai metodi formali. - Il linguaggio delle espressioni regolari come linguaggio di sistemi reattivi. - Calculus of Communicating Systems (CCS) di Milner: sintassi e semantica operazionale. - Equivalenze: bisimulazione strong e weak. - Congruenza osservazionale e sua decidibilità. - Varianti (con tempo, con località, etc.) del CCS. - Linguaggi per la valutazione delle performance.

- R. Milner: A Calculus of Communicating Systems. LNCS 92, Springer (1980).

- A. Aldini, M. Bernardo, F. Corradini: A Process Algebraic Approach to Software Architecture Design. Springer (2009).

- Altre letture ad articoli di ricerca, selezionati durante il corso.

Sviluppo di un progetto svolto in gruppi.