MODELLAZIONE E VERIFICA DI SISTEMI SOFTWARE

Obiettivi formativi:

Questo insegnamento ha lo scopo di introdurre tecniche per modellare l'architettura di sistemi software complessi e verificarne le proprietà attraverso l'uso di metodi formali basati su linguaggi, automi, logiche ed algebre.

Settore scientifico-disciplinare:

INF/01.

Crediti:

12.

Modulo:

Unico.

Durata:

Annuale, 112 ore (80 di lezione teorica + 32 di esercitazione guidata).

Frequenza:

Consigliata, ma non obbligatoria.

Docente:

Dott. Alessandro Aldini.

Programma:

01. Introduzione alla modellazione e verifica:
      01.01 L'esigenza di metodi formali nello sviluppo del software.
      01.02 Linguaggi formali ed automi.
      01.03 Grammatiche a struttura di frase e classificazione di Chomsky.
      01.04 Approcci formali alla semantica dei linguaggi.
      01.05 Teoria della concorrenza, logiche ed algebre.

02. Linguaggi regolari e automi a stati finiti:
      02.01 Automi a stati finiti deterministici.
      02.02 Automi a stati finiti non deterministici.
      02.03 Automi a stati finiti con ε-transizioni.
      02.04 Minimizzazione ed equivalenza per automi a stati finiti.
      02.05 Relazione tra automi a stati finiti e grammatiche lineari destre.
      02.06 Proprietà dei linguaggi regolari e pumping lemma.
      02.07 Espressioni regolari.
      02.08 Relazione tra espressioni regolari e automi a stati finiti.

03. Linguaggi liberi e automi a pila:
      03.01 Grammatiche libere e alberi sintattici.
      03.02 Grammatiche libere in forma normale di Chomsky.
      03.03 Proprietà dei linguaggi liberi e pumping lemma.
      03.04 Automi a pila e relazione con grammatiche libere.
      03.05 Parsing top-down.
      03.06 Parsing bottom-up.

04. Semantica denotazionale:
      04.01 Semantica denotazionale di un linguaggio imperativo.
      04.02 Semantica denotazionale con blocchi e procedure.

05. Semantica operazionale:
      05.01 Semantica operazionale naturale di un linguaggio imperativo.
      05.02 Semantica operazionale naturale con blocchi e procedure.
      05.03 Semantica operazionale strutturata di un linguaggio imperativo.

06. Logiche temporali e model checking:
      06.01 Modelli di Kripke.
      06.02 Logiche temporali.
      06.03 Logiche linear-time vs. logiche branching-time.
      06.04 Algoritmi di model checking.

07. Algebre di processi ed equivalenze comportamentali:
      07.01 Concorrenza e nondeterminismo.
      07.02 Sintassi e semantica di operatori comportamentali.
      07.03 Equivalenza basata su tracce.
      07.04 Equivalenza basata su bisimulazione.
      07.05 Equivalenza basata su test.

08. Linguaggi per la descrizione di architetture software:
      08.01 Componenti, connettori e stili architetturali.
      08.02 Sintassi di un linguaggio architetturale basato su algebra di processi.
      08.03 Semantica di un linguaggio architetturale basato su algebra di processi.
      08.04 Conformità comportamentale.
      08.05 Estensioni topologiche.

09. Attività di laboratorio:
      09.01 Modellazione di sistemi software tramite strutture di Kripke.
      09.02 Modellazione di sistemi software tramite linguaggi architetturali.
      09.03 Esercizi su model checking.
      09.04 Esercizi su equivalence checking.

Testi di riferimento:

  • Hopcroft, Motwani, Ullman, "Automi, Linguaggi e Calcolabilità", Addison-Wesley, 2009
               (Hopcroft, Motwani, Ullman, "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley, 2007)
               (copre le sezioni 02 e 03 del programma).
  • Nielson, Nielson, "Semantics with Applications: An Appetizer", Springer, 2007
               (copre le sezioni 04 e 05 del programma).
  • Clarke, Grumberg, Peled, "Model Checking", MIT Press, 1999
               (copre la sezione 06 del programma).
  • Aldini, Bernardo, Corradini, "A Process Algebraic Approach to Software Architecture Design", Springer, 2010
               (copre le sezioni 07 e 08 del programma).
    		•

    Propedeuticità:

    Programmazione Procedurale e Logica, Matematica Discreta.

    Modalità didattiche:

    Lezioni teoriche ed esercitazioni guidate in laboratorio (materiale didattico).

    Modalità di accertamento:

    Progetto individuale e prova scritta.

    Commissione d'esame:

    Dott. Alessandro Aldini e Prof. Marco Bernardo (supplente: Prof. Alessandro Bogliolo).

    Note:

    Il progetto individuale, che è associato ad una ed una sola prova scritta e va consegnato il giorno della prova, viene valutato in decimi attraverso la sua discussione.
    La prova scritta viene valutata in ventesimi.
    Il voto finale è determinato dalla somma dei voti del progetto e della prova scritta.

    Ultima modifica: 09/10/2012 Approvato da: Presidente CCdL