Reti e Sistemi Informatici


Verifica dei processi concorrenti

1. Prerequisiti

  • Competenze attese in ingresso (richieste all'inizio del corso)
    • Competenze e conoscenze della laurea L31, con particolare attenzione alla capacita' di astrazione e alla conoscenza dei principi di base della concorrenza.

    • Eventuali corsi propedeutici (forniscono le "competenze attese in ingresso")

      Corso di base su linguaggi formali e sistemi operativi (parte sui processi e sulla comunicazione). IL corso di MCAD (modelli concorrenti e algoritmi distribuiti) non è propedeutico, ma lo studente/studentessa che segua entrambi i corsi potrà sicuramente avere una migliore visione di insieme degli argomenti dei due corsi.


2. Obiettivi formativi - Learning objectives

  • Obiettivo del corso e' di fornire gli strumenti, teorici e pratici, necessari alla verifica dei sistemi, ed in particolare del software. Per raggiungere tale obiettivo studieremo alcuni paradigmi di base per la specifica di processi distribuiti, focalizzando l'attenzione sulle capacità modellistiche e sugli strumenti di verifica di proprietà di buon comportamento. Studieremo inoltre la verifica dei sistemi in cui il corretto funzionamento dipende da caratteristiche di tempo.

    In particolare il corso ha come obiettivo di far acquisire le competenze teoriche legate ai modelli della concorrenza e di farle applicare per risolvere problemi concreti di verifica del software. Le modalità di insegnamento favoriranno l'acquisizione, da parte degli studenti, di capacità autonoma di apprendimento, (comprensione di articoli scientifici sugli argomenti del corso), di abilità comunicative (relazioni associate agli esercizi di laboratorio e discussioni in classe) e di autonomia di giudizio (grazie a laboratori in cui gli studenti debbono organizzare esperimenti e valutazione delgi stessi)

 

3. Risultati dell'apprendimento attesi

  • Competenze attese in uscita (acquisite durante il corso)

    Alla fine del corso lo studente sara' in grado di specificare sistemi concorrenti usando linguaggi formali e di utilizzare strumenti software per la verifica di proprieta' del sistema tramite verifica di proprieta' del modello. In particolare lo studente acquisirà famigliarità con i seguenti strumenti: GreatSPN, NuSMV e Uppaal. Oltre alle classiche proprieta' dei sistemi distribuiti quali assenza di deadlock, fairness e liveness, lo studente sara' in grado di definire e verificare proprieta' in logica temporale quali ad esempio: "se il processo P manda un messaggio, allora non inviera' il prossimo messaggio sino a che non riceve un acknowledgment", oppure "se il processo P manda un messaggio, ricevera' un acknowledge entro 5 unita' di tempo"

 

4. Programma - Course Syllabus

  • Italiano
    • Introduzione alla verifica dei sistemi
    • Un primo linguaggio di specifica, le Reti di Petri (reti posto transizione e reti colorate): definizione, proprieta' e tool disponibili (GreatSPN).
    • Un secondo linguaggio di specifica, le algebre dei processi: definizione, proprieta' di CCS e CSP
    • Esprimere proprieta': le logiche temporali lineari (LTL) e branching (CTL) e i relativi tool (NuSMV e RGMEDD)
    • Esprimere il tempo: gli automi temporizzati, le logiche branching temporizzate e relativi tool (Uppaal)


 

5. Modalità di verifica dell'apprendimento

Il corso ha due modalità di esame, a scelta dello studente/studentessa, a seconda che egli/ella voglia approfondire maggiormente gli obiettivi formativi legati agli aspetti di definizione e confronto dei paradigmi di modellazione concorrente o gli aspetti legati agli strumenti di verifica. Tipo 1: esame orale su argomenti di base del corso e un set esteso di esercizi di laboratorio da discutere con il docente Tipo 2: esame orale su tutti gli argomenti del corso e un insieme ridotto di esercizi di laboratorio da discutere con il docente Per l'esame di tipo 1 la valutazione è basata per l'80% sul laboratorio, ma è comunque richiesta la sufficienza anche nella parte di esame orale per poter superare l'esame. Per l'esame di tipo 2 la valutazione è basata per l'80% sull'orale, ma è comunque richiesta la sufficienza anche nella parte di laboratorio per poter superare l'esame. L'individuazione degli argomenti di base per l'esame di tipo 1 avviene durante il corso, alla fine di ogni macro argomento e viene pubblicato sul sito moodle del corso. Gli esercizi di laboratorio vengono assegnati durante il corso (nella forma "lunga" per l'esame di tipo 1, e nella forma "corta" per l'esame di tipo 2). Gli esercizi sono resi disponibili sul sito moodle del corso.

5.1 Controllo dell'apprendimento durante il corso

Esercizi assegnati dal docente e discussi in classe. Verranno inoltre assegnati dei mini progetti da svolgersi con l'ausilio degli strumenti software di verifica appresi durante il corso. Gli studenti sono invitati a consegnare i mini progetti a precise scadenze, in modo da poter discutere in aula delle difficoltà incontrate. I mini progetti, e le associate relazioni, sono valutati contestualmente all'esame finale.

 

6. Modalità d'insegnamento

Lezioni frontali, con utilizzo di strumenti di verifica da parte del docente. Durante il corso vengono assegnati esercizi e mini progetti che gli studenti sono invitati a svolgere durante il corso, a scadenze concordate. Almeno 12 ore vengono dedicate a lezioni/laboratorio in cui vengono presentati gli strumenti di verifica e vengono discussi i problemi che gli studenti hanno incontrato nello svolgimento dei mini progetti. In queste lezioni gli studenti sono invitati a presentare le loro soluzioni che vengono discusse dal docente e dagli altri studenti


 

7. Testi consigliati e bibliografia - Reading materials

1. Doron Peled, Software Reliability Models, Springer and Verlag, ISBN: 978-1-4419-2876-4 (Print) 978-1-4757-3540-6 (Online)

2.Christel Baier and Jost-Pieter Katoen, Model Checking – MIT Press