Ingegneria del software: specifiche di processi distribuiti
 (6 crediti, laurea specialistica., primo periodo didattico)

Docente: Susanna Donatelli,
                   tel:  0116706746
                    e-mail: susi@di.unito.it
                    orario di ricevimento: mercoledi' 16-16.45, venerdi' 16-17.15 o su appuntamento
 
 
Esercizi per l'A.A. 2003/2004

Descrizione del corso. Il corso fornisce 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.

Argomenti trattati.

Competenze acquisite dallo studente a fine 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. 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
                  ricevera' il prossimo messaggio sino a che non riceve un acknowledgment", oppure "ad ogni trasmissione
                  di messaggio segue una risposta entro 5 unita' di tempo".

Strumenti usati:
                GreatSPN  (vedi link)
                  Manuale di GreatSPN manuale.pdf
                 Uppaal       (vedi link)

Modalità d'esame.  L'esame si svolge con una prova orale sui contenuti del corso e su di un
                eventuale approfondimento monografico concordato sulla base degli interessi del singolo studente,
                che potra' essere sostituito da un esercizio di verifica svolto con uno dei tool messi a disposizione
                  dal docente per la verifica di sistemi specificati con reti di Petri, algebre di processi o automi temporizzati.
                  Per gli studenti  che hanno seguito il corso nell.'A.A. 03/04 le modalita' di esame sono cambiate: non                 c'e' piu' l'approfondimento, ma degli esercizi uguali per tutti, che trovate a inizio di questa pagina
 

Relazioni con altri corsi. E' un naturale complemento del corso  di Ingegneria del
                Software, anche se non è richiesta una propedeuticità stretta. Il corso si inserisce in modo
                naturale nei piani di studio orientati alla progettazione di sistemi e di applicazioni distribuite. È
                anche di interesse per i piani di studio sui modelli computazionali, come introduzione agli
                aspetti modellistici connessi ai processi distribuiti. Si consiglia di seguirlo dopo i due moduli
                obbligatori di sistemi operativi e nel terzo/quarto anno del nuovo ordinamento, poichè
                fornisce elementi di base utili ad altri moduli specialistici (ad es. Simulazione, Sistemi
                Informativi, Modelli Markoviani).
   
Riferimenti utili  

  • Sito web delle reti di Petri  www.daimi.au.dk/PetriNets

    • Programma dettagliato del corso

    RP1: Capitolo 2 del MATCH book (disponibile in biblioteca - dispense) capitolo2: reti untimed
    RP2: Capitolo 6 del MATCH book (disponibile in biblioteca - dispense) capitolo6: analisi di Reti di Petri
    PA1: Capitolo 5 del MATCH book (disponibile in biblioteca - dispense) capitolo5: algebra dei processi stocastici
    SRM: Libro  di Doron Peled: "Software reliability methods", ed. Springer (in prestito settimanale in biblioteca)
    MC: Dispense di Jost-Pieter Katoen: "Concepts algorithms and tools for model checking" (disponibile in biblioteca - dispense)
     

  • Introduzione alla validazione dei sistemi e dei programmi

    •    SRM capitolo 1 (11 pagine). SRM capitolo 2 e' un riassunto di concetti preliminari che gli studenti dovrebbero gia' avere
        acquisito in altri corsi, sono 15 pagine che possono costituire un buon ripasso sui "fondamentali"
        MC capitolo 1 (escluso 1.6) (17 pagine)
     
  • Reti di Petri

    •      RP1: 2.1, 2.2, 2.3 (sino a equal conflict e free-choice incluso), 2.4 (escluso il paragrafo su "concurrent semantics"),
                    2.5 (sino alla definizione 2.17 inclusa) (circa 38 pagine)
         RP2: 6.1, 6.2, 6.3 (escluso l' esempio 6.3), 6.4.1, 6.5 (solo pagina 22, ultimi due paragrafi di pagina 23, pagina 24 sino a 6.5.1,
                    esempio 6.9) .   (circa 20 pagine) Il resto del capitolo e' un possibile argomento di approfondimento.
     
  • Algebra dei processi

    •     SRM capitolo 8 (tutto escluso 8.9) (circa 30 pagine)
          PA1: 5.1, 5.2 (tranne 5.2.4) (circa 15 pagine, in parte ripetono concetti gia' presenti in SRM)
     
     
  • Model checking PLTL

    •    SRM, capitolo 5: 5.1, esempio della molla dal 5.2, tutto il 5.4 tranne il paragrafo sulla fairness)  (circa 8 pagine)
        SRM, capitolo 6: 6.7, 6.14, 6.15 (circa 4 pagine)
        MC, capitolo 2: 2.1, 2.2, 2.3, 2.5 (solo il primo esempio, quello sul canale di comunicazione), 2.10, 2.11 (circa 22 pagine)
         Gli argomenti in MC sono in parte ripetuti, o esemplificati in SRM.
        Il resto del capitolo 2 di MC e' un possibile argomento di approfondimento.
     
  • Model checking CTL

    •     MC:  capitolo 3 (sino a 3.4 incluso, 3.6, 3.7, 3.8 dal paragrafo sulla complessita',  3.9, 3.10)  (circa 40 pagine)
           Il resto del capitolo 3 di MC e' un possibile argomento di approfondimento.
     
  • Model checking TCTL

    •      MC:  capitolo 4 (sino a 4.6 escluso, e 4.9 (senza esempio)
          Il resto del capitolo 4 di MC e' un possibile argomento di approfondimento, insieme all' articolo di hezinger di cui ho lasciato
           una copia in biblioteca.