Modelli Formali e Analisi di Sistemi - a.a. 2015-16

Corso di Laurea Magistrale in Informatica

Docente

Alessandro Bianchi
Dipartimento di Informatica - V Piano
Tel. 080 544 2283
Email alessandro.bianchi@uniba.it
Pagina Web http://www.di.uniba.it/~bianchi/

Ricevimento studenti:

• mercoledì dalle 15.30 alle 17.30 - Dipartimento di Informatica - Bari;
• ora e luogo definiti per appuntamento.

Il Corso

Orario: in attesa dell'orario definitivo delle lezioni, il corso si terrà nel laboratorio von Neumann il mercoledì dalle 8:30 alle 10:30. Dopo il 16/10, data ultima per segnalare alla Prof.ssa Roselli e al Prof. Semeraro l'elenco degli insegnamenti a scelta, le lezioni riprenderanno con 6 ore settimanali in orario che sarà comunicato in seguito.

Obiettivi: Il corso si focalizza su alcuni modelli formali particolarmente adatti a descrivere sistemi critici ad elevata complessità. Tali modelli favoriscono l'analisi di un insieme di proprietà particolarmente interessanti dal punto di vista computazionale, sia di natura generale, come ad esempio deadlock e livelock, starvation e liveness, reachability, reversibility, sia di natura dipendente dal dominio applicativo, come ad esempio la sicurezza nei protocolli di comunicazione o la consapevolezza che un nodo ha relativamente all'esistenza di altri nodi in reti MANET.
Ha inoltre lo scopo di fornire le competenze fondamentali per applicare i concetti discussi nella risoluzione dei problemi.
E' richiesto che gli studenti abbiano le conoscenze di base fornite nei corsi triennali della classe di Informatica, e abbiano sviluppato capacità di astrazione e formalizzazione. Condizione necessaria per seguire proficuamente il corso è il desiderio di applicare le conoscenze per indagare fenomeni che si presentano in pratica.
Il corso è organizzato ponendo in stretta relazione lo studio dei modelli formali introdotti con i problemi ricorrenti in alcuni esempi (reti mobili ad-hoc - MANET, gestione dei job nei sistemi Grid, protocolli di sicurezza, e così via). L'obiettivo di tale organizzazione è quello di mostrare come un'opportuna modellazione favorisca l'analisi delle proprietà specifiche del sistema modellato.
Per ulteriori dettagli, si rimanda al Sillabo del corso.

Bibliografia

• E. Börger, R. Stärk, Abstract State Machine, Springer 2003
• C.A.R. Hoare, Communicating Sequential Processes, Prentice Hall International, 1985 (disponibile in http://www.usingcsp.com./cspbook.pdf)
• R. David, H. Alia, Discrete, Continuous, and Hybrid Petri Nets, Springer 2003
• R. Milner, Communication and Concurrency, Prentice Hall International 1995
• AA.VV. The Go Programming Language, (disponibile sul sito http://golang.org)
• AA.VV. Erlang Programming Language, (disponibile sul sito http://www.erlang.org)
• Articoli e lucidi riferiti / distribuiti durante le lezioni.

Strumenti software utili

• CPN Tools;
• COREAsm.

Aggiornamenti e Avvisi

• 1 dicembre 2015 Si avvisa che a causa dei preannunciati impegni del docente, e a causa della chiusura dell'ateneo, le lezioni seguiranno il seguente calendario:
  • venerdì 4 dicembre: lezione regolare, sulla discussione degli approfondimenti proposti dagli studenti e sull'analisi della starvation;
  • lunedì 7 dicembre: chiusura dell'ateneo e sospensione delle attività didattiche;
  • venerdì 11 dicembre: niente lezione;
  • lunedì 14 dicembre: niente lezione;
  • venerdì 18 dicembre: lezione regolare con inizio alle ore 9.00, sull'astrazione dei predicati degli stati ASM e sulla modellazione di N-AODV;
  • venerdì 8 gennaio: lezione regolare di conclusione del corso.
• 23 novembre 2015 Nella pagina del programma sono pubblicate le dispense relative all'introduzione a CSP, agli operatori per il parallelismo e all'esempio di modellazione di protocolli di sicurezza con il CSP.
• 10 novembre 2015 Nella pagina del programma sono pubblicate le dispense relative alle DASM, all'analisi delle proprietà mediante ASM, e ad alcuni esempi di applicazione di ASM. Inoltre sono pubblicate le dispense dei seminari che terrà il Dott. Gennaro Vessio.
• 3 novembre 2015 Nella pagina del programma sono pubblicate le dispense relative all'introduzione alle ASM, ai loro fondamenti e al metodo ASM.
• 21 ottobre 2015 Nella pagina del programma sono pubblicate le dispense relative alle Reti di Petri.
• 7 ottobre 2015 Nella pagina del programma sono pubblicate le dispense relative all'introduzione alle MANET e all'introduzione alle Grid.
• 30 settembre 2015 Questa pagina è stata aggiornata con l'indicazione dell'orario delle prime lezioni. Inoltre, nella pagina del programma sono pubblicate le dispense relative alle proprietà computazionalmente interessanti.
• 23 settembre 2015 Questa pagina è on line. Inoltre, nella pagina del programma sono pubblicate le dispense relative all'introduzione al corso.