Schema della sezione

    Minimizza tutto Espandi tutto

  • Introduzione

  • Informazioni generali

    Le lezioni di questo modulo cominceranno lunedì 3 ottobre 2022. Le lezioni si tengono il lunedì e il giovedì dalle 15:30 alle 18:30, ma in alcune date termineranno alle 17:30. Le lezioni saranno esclusivamente in presenza; quando possibile, il materiale relativo a una lezione sarà pubblicato in anticipo. Saranno anche disponibili le registrazioni delle lezioni dell'anno scorso sugli stessi argomenti.

    Questo è il calendario delle prime lezioni, dedicate alle tecniche di dimostrazioni di correttezza di programmi e alla logica di Hoare. Consultate sempre il sito per eventuali variazioni.

    •  3 ottobre, 15:30-18:30, aula U4-02
    •  6 ottobre, 15:30-17:30, aula U24-C1
    • 10 ottobre, 15:30-18:30, aula U4-02
    • 13 ottobre, 15:30-18:30, aula U24-C1
    • 17 ottobre, 15:30-17:30, aula U4-02

    Calendario delle lezioni dedicate ai modelli di sistemi concorrenti: CCS
    • 20 ottobre, 15:30-18:30, aula U24-C1
    • 24 ottobre, 15:30-17:30, aula U4-02
    • 27 ottobre, 15:30-16:30, aula U24-C1
    • 3 novembre, 15:30-18:30, aula U24-C1
    • 7 novembre, 15:30-18:30, aula U4-02
    • 10 novembre, 15:30-18:30, aula U24-C1
    • 14  novembre, 15:30-18:30, aula U4-02

    Calendario delle lezioni dedicate ai modelli di sistemi concorrenti: reti di Petri
    • 17 novembre, 15:30-18:30, aula U24-C1
    • 21 novembre, 15:30-18:30, aula U4-02
    • 24 novembre, 15:30-18:30, aula U24-C1
    • 28 novembre, 15:30-18:30, aula U4-021
    • 1 dicembre, 15:30-18:30, aula U24-C1
    Calendario delle lezioni su logiche temporali e model-checking (consultate sempre il sito per eventuali variazioni)
    • 5 dicembre 15:30-17:30, aula U4-02
    • 12 dicembre 15:30-17:30, aula U4-02
    • 15 dicembre 15:30-17:30, aula U24-C1
    • 19 dicembre 15:30-17:30, aula U4-02
    • 22 dicembre 15:30-17:30, aula U24-C1
    • 9 gennaio 15:30-17:30, aula U4-02
    In preparazione all'esame, si potranno tenere incontri supplementari

  • Esami

    La prova scritta comprende quattro esercizi, uno per ciascuno dei seguenti argomenti:

    • CCS e bisimulazione
    • Reti di Petri e processi
    • Dimostrazioni di correttezza con la logica di Hoare
    • Logiche temporali e model-checking
    Negli esempi di prove scritte che trovate in questa sezione è presente un quinto esercizio, di traduzione dall'italiano a logiche temporali; questo tipo d'esercizio non fa più parte della prova scritta, ma può essere argomento di domande durante il colloquio.
    • Cartella
      Esempi di temi d'esame Cartella
    • File
      Appello del 6 febbraio 2023 File

      Testo della prova scritta

    • Prenotazione
      Appello di giugno - prova scritta Prenotazione

      Gli studenti che intendono sostenere la prova del modulo Modelli della concorrenza nell'appello del 13 giugno 2023 sono pregati di compilare questo modulo entro il 10 giugno. Chi prevede di completare l'esame dell'insegnamento Modelli e computabilità in questo appello deve anche iscriversi all'esame sul sito delle segreterie online.

    • Prenotazione
      Appello di luglio - prova scritta Prenotazione

      Gli studenti che intendono sostenere la prova del modulo Modelli della concorrenza nell'appello del 4 luglio 2023 sono pregati di compilare questo modulo entro il 30 giugno. Solo chi prevede di completare l'esame dell'insegnamento Modelli e computabilità in questo appello deve anche iscriversi all'esame sul sito delle segreterie online.

    • Pagina
      Appello del 3 luglio 2023 Pagina

      Esito della prova scritta e calendario degli orali

    • Prenotazione
      Appello di settembre Prenotazione

      Gli studenti che intendono sostenere la prova del modulo Modelli della concorrenza nell'appello dell'11 settembre 2023 sono pregati di compilare questo modulo entro l'8 settembre. Solo chi prevede di completare l'esame dell'insegnamento Modelli e computabilità in questo appello deve anche iscriversi all'esame sul sito delle segreterie online.

  • Dimostrazioni di correttezza

    Come si può stabilire se un programma è "corretto"? In questa parte del corso si studia un metodo rigoroso per esprimere i requisiti di programmi sequenziali e per dimostrare che un programma soddisfa un requisito assegnato. Lo strumento fondamentale è la logica di Hoare, definita a partire dalla logica proposizionale e dei predicati.

    • Pagina
      Materiale di studio Pagina
    • Cartella
      Lezione del 3 ottobre 2022 Cartella

      15:30-18:30, aula U4-02

      Riassunto della lezione
      • Introduzione generale al modulo (vedi Introduzione)
      • Esempio di dimostrazione di correttezza informale (vedi Dimostrazione informale)
      • Nozioni fondamentali di logica proposizionale, prima parte (vedi Logica proposizionale)
    • Cartella
      Lezione del 6 ottobre 2022 Cartella

      15:30-17:30, aula U24-C1

      Il materiale di consultazione non è ancora completo.

      Riassunto

      • Ripasso di logica proposizionale, seconda parte (vedi Logica proposizionale nel materiale della prima lezione)
      • Una logica per ragionare su programmi: le triple di Hoare
      • Definizione di un linguaggio di programmazione
      • Regole di derivazione della logica di Hoare, prima parte (vedi Logica di Hoare, prima parte; attenzione: nella definizione delle espressioni aritmetiche manca la clausola che dice che ogni nome di variabile è un'espressione aritmetica)
    • Cartella
      Lezione del 10 ottobre Cartella

      15:30-17:30, aula U4-02

      Riassunto della lezione

      • Regole di derivazione della logica di Hoare, seconda parte
      • La regola delle istruzioni iterative: definizione di invariante di ciclo
      • Distinzione fra correttezza parziale e correttezza totale
      • Esercizi
    • Cartella
      Lezione del 13 ottobre 2022 Cartella

      15:30-18:30, aula U24C1

      Il contenuto di questa cartella verrà arricchito nei prossimi giorni.

      Riassunto

      • Logica di Hoare: la regola di derivazione per la correttezza totale di istruzioni iterative
      • Considerazioni su correttezza e completezza della logica di Hoare
      • Precondizione più debole (weakest precondition): definizione, significato intuitivo, esempi
      • Corrispondenza fra stati e formule
    • File
      Esercizi svolti File

      Dimostrazioni di correttezza e precondizioni più deboli

    • Cartella
      Lezione del 17 ottobre Cartella

      15:30-17:30, aula U4-02

      Riassunto

      • Programmi come trasformatori di stato; computazione come cammino in un grafo
      • Schema generale di una dimostrazione di correttezza
      • La logica di Hoare nella pratica: design by contract, Eiffel, Java Modeling language
      • La logica di Hoare come fondamento di una semantica dei programmi
      • Esercizi
      Attenzione: nel diagramma a pagina 7 del file mdc-finale.pdf la regione associata alla formula "s" dovrebbe contenere tutti gli stati nell'intersezione di "i" e "non B".

  • Modelli di sistemi concorrenti - CCS

    Presentiamo un linguaggio (CCS - Calculus of Communicating Systems) con il quale è possibile specificare, in forma astratta, sistemi concorrenti, cioè formati da componenti che interagiscono. Studiamo una nozione di equivalenza fra "programmi" scritti in questo linguaggio, e il suo interesse, sia teorico sia applicativo.

    • Lezione del 20 ottobre 2022, ore 15:30-18:30, aula U24-C1

      Dalla programmazione sequenziale a quella concorrente: i sistemi reattivi; problematiche relative alla semantica.  Introduzione al Calcolo dei sistemi comunicanti (CCS). I sistemi di transizioni etichettati (LTS): definizioni. La sintassi del CCS puro e la sua semantica come LTS attraverso regole di inferenza.

    • File
      appunti_della lezione_22ottobre22 File

    • Lezione del 24 ottobre 2022, ore 15:30-17:30, aula U4-02

      Il CCS puro sintassi e semantica  tramite LTS. L'esempio del produttore e consumatore con buffer a una posizione: la specifica in CCS e il sistema di transizioni associato. Requisiti per una nozione di equivalenza per i sistemi reattivi: congruenza rispetto agli operatori. Equivalenza rispetto alle Tracce:definizione formale e discussione rispetto alla possibilità di generare deadlock (si veda l'esempio delle due macchinette del caffè).

    • File
      appunti_della lezione_24_ottobre_22 File

    • Lezione del 27 ottobre 2022, ore 15:30-16:30, aula U24-C1 

      Bisimulazione (forte). Definizione formale e discussione su esempi.

    • File
      appunti_della lezione_27_ottobre_22 File

    • Lezione del 3 novembre 2022, ore 15:30-18:30, aula U24-C1

      Bisimulazione forte, esempi (confronto tra buffer a due posizioni e composizione parallela di due buffer a una posizione) La Bisimulazione forte è una congruenza rispetto agli operatori del CCS. 

      Relazione di transizione debole, equivalenza rispetto alle Tracce debole; Bisimulazione debole. Discussione su esempi.

      La verifica della Bisimulazione con il gioco "attaccante-difensore".

    • File
      slide sulla Bisimulazione debole e il gioco per verificarla File

    • Lezione del 7 novembre 2022, ore 15:30-18:30, aula U4-02

      Relazioni tra equivalenza rispetto alle Tracce e Bisimulazione forte e debole.
      Processi deterministici ed equivalenze.
      Esercizi sulla verifica della bisimulazione. (si vedano le slide 13, 14 e 15 del file  "Bisimulazione e congruenza")

    • File
      Bisimulazione debole proprietà - slide File

    • Lezione del 10 novembre 2022, ore 15:30-18:30, aula U24-C1

      La Bisimulazione debole è una congruenza rispetto agli operatori del CCS tranne che rispetto all'operatore + e alla ricorsione.
      Bisimulazione e Relazione di congruenza definita con Assiomi.
      Esercizi sulla Bisimulazione come gioco

    • File
      Bisimulazione e congruenza File
    • File
      Esercizi sulla verifica della Bisimulazione - da svolgere File

      Questi esercizi verranno corretti lunedì 14 novembre.

    • Lezione del 14 novembre 2022, ore 15:30-18:30, aula U4-02

      Soluzione degli esercizi assegnati sulla verifica della Bisimulazione.
      Discussione su semantica a "interleaving" del CCS e ipotesi di atomicità delle azioni.
      La specifica di un protocollo di comunicazione con CCS e con reti di Petri.

    • File
      soluzioni degli esercizi sulla verifica della Bisimulazione File
    • File
      lez 14 nov File
    • File
      la specifica di un protocollo di comunicazione File

    • -------------------------------------------

      Materiale per questo argomento

    • Pagina
      Reactive Systems: Modelling, Specification and Verification Pagina
    • File
      Bisimulazione debole e il gioco per la sua verifica File

      Per la verifica della bisimulazione con la tecnica tratta dalla teoria dei giochi dell'"attaccante e difensore" si veda anche la sezione 3.5 e 3.5.1 del testo  "Reactive Systems" al link precedente. (Si noti che viene presentata la tecnica per la Bisimulazione forte e solo nella sezione 3.5.1 quella per la Bisimulazione debole.) 

    • File
      Bisimulazione, esempi File
      Alcuni di questi esercizi sono stati discussi a lezione

    • Letture

    • File
      C.A.R. Hoare, Communicating Sequential Processes, 1978 File
    • File
      R. Milner, Elements of Interactions File
    • File
      caal_tutorial File

      Caal è un tool open source sviluppato presso l'Università di  Aalborg, in Danimarca e disponibile al link: https://caal.cs.aau.dk/. Consiste di vari moduli tra cui un editor per CCS, uno per la visualizzazione dei processi, uno per la verifica delle equivalenze e il model checking e uno per il gioco della bisimulazione. Questo file presenta gli aspetti fondamentali del tool e contiene indicazioni su come utilizzarlo.

  • Modelli di sistemi concorrenti - Reti di Petri

    Le reti di Petri costituiscono un modello formale per rappresentare sistemi distribuiti e processi concorrenti a partire dalla nozione di stato locale. Studiamo i fondamenti della teoria delle reti di Petri, e alcune tecniche per analizzarne le caratteristiche.

    • Lezione del 17 novembre 2022, ore 15:30-18:30, aula U24-C1

      Le reti di Petri: introduzione, l'esempio del "produttore e consumatore". Definizione formale di: rete elementare, pre-set e post-set di un elemento e di un insieme di elementi; evento abilitato in una configurazione o caso; regola di scatto di un evento; relazione di indipendenza tra eventi; scatto di un insieme di eventi indipendenti (passo).  L'insieme dei casi raggiungibili di un sistema elementare e il grafo dei casi raggiungibili.
      La "diamond property" e la sua prova. Grafo sequenziale e isomorfismo tra grafi dei casi.  Il problema della sintesi di un sistema elementare da un sistema di transizioni etichettato. (Si veda la prima parte delle slide "reti di Petri 1").

    • Lezione del 21 novembre 2022, ore 15:30-18:30, aula U4-02

      Sistemi elementari, situazione di "Contatto"e eliminazione. Sistemi senza contatto e, la nuova regola di scatto. Relazioni tipiche tra eventi in un caso raggiungibile: sequenza, concorrenza, conflitto e confusione. L'esempio della mutua esclusione nella condivisione di una risorsa.
      Discussione su eventi sincroni, asincroni, alternati.
      Tipiche operazioni di composizione di reti elementari. (Si veda la seconda parte delle slide "reti di Petri 1").
      Semantica ad ordini parziali - Reti di occorrenze e ordini parziali: relazione co, li, co-set, li-set, tagli e linee. K-densità. Esempi e interpretazione di linee e tagli. (Si veda la prima parte delle slide "I processi non sequenziali").

    • Lezione del 24 novembre 2022, ore 15:30-18:30, aula U24-C1

      Processi del sistema "mutua esclusione".  I processi non sequenziali dei sistemi elementari finiti, definizione formale e proprietà (ogni linea attraversa ogni taglio, cioè la rete di occorrenze è K-densa; ogni B-taglio (taglio di condizioni) corrisponde ad un caso raggiungibile del sistema.
      I processi ramificati e l'unfolding dei sistemi elementari. (Si veda la seconda parte delle slide "I processi non sequenziali").
      Esercizi sui sistemi elementari e sul grafo dei casi raggiungibili.

    • Lezione del 28 novembre 2022, ore 15:30-18:30, aula U4-02

      Dalle reti elementari alle reti Posti e Transizioni e reti ad alto livello (reti colorate).
      Le proprietà di comportamento e una panoramica della teoria delle reti di Petri per la loro verifica.
    • File
      Da reti elementari a reti PT e a reti colorate - proprietà di comportamento File

    • Lezione del 1 dicembre 2022, ore 15:30-18:30, aula U24-C1

    • File
      esercizi sui processi File
      questi esercizi sui processi non sequenziali verranno corretti il 1 dicembre
    • File
      Esercizio sulla bisimulazione File

      questo esercizio verrà corretto in aula l'1 dicembre

    • -------------------------------------------

      Materiale per questo argomento

    • File
      Reti di Petri 1 -slide File
    • File
      Soluzione degli esercizi sui sistemi elementari e il grafo dei casi File
    • File
      I processi non sequenziali - slide File
      aggiornato il 24 nov '22
    • File
      soluzioni degli esercizi sui processi File
    • File
      G. Rozenberg, J. Engelfriet; Elementary Net Systems File

      Di questo articolo si considerino in particolare (senza le dimostrazioni) le seguenti sezioni:
      - sez 1, 2, 3 
      - 4.1 (fino al teorema 29 compreso), 4.5 
      - 5, 5.1, 5.2, 5.3, sui processi non sequenziali si vedano anche le slide pubblicate.

    • File
      J. Klein, M. Koutny; Elementary Net Systems File

      articolo su Elementary net systems e processi non sequenziali

    • Letture

    • File
      T.Murata: "Petri nets: Properties, Analysis and Applications.” File

      Articolo su una panoramica della teoria e delle applicazioni delle Reti di Petri

    • URL
      Carl Adam Petri - Life and Science, Einar Smith, Springer URL

      Una biografia di C.A. Petri

    • File
      L'eredità di C.A. Petri: dagli automi alla comunicazione File

      articolo sui fondamenti della teoria delle reti di Petri

  • Logiche temporali e model-checking

    Fissato un modello formale di un sistema, reale o da realizzare, vogliamo stabilire se il modello soddisfa certi requisiti. Le tecniche di model-checking si basano sull'impiego di logiche modali e temporali per esprimere le proprietà che vogliamo studiare, e su algoritmi che decidono se il modello del sistema in esame le soddisfa o no. Studiamo alcuni linguaggi logici e i relativi algoritmi di decisione.