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.

English version: The objective of this course is to introduce techniques for modeling the architecture of complex software systems and verifying their properties by means of formal methods based on languages, automata, logics, and algebra.

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.

English version:

01. Introduction to modeling and verification:
      01.01 The need for formal methods in software development.
      01.02 Formal languages and automata.
      01.03 Grammars and Chomsky classification.
      01.04 Formal approaches to language semantics.
      01.05 Concurrency theory, logics, and algebra.

02. Regular languages and finite-state automata:
      02.01 Deterministic finite-state automata.
      02.02 Nondeterministic finite-state automata.
      02.03 Nondeterministic finite-state automata with epsilon-transitions.
      02.04 Minimization and equivalence for finite-state automata.
      02.05 Finite-state automata and linear grammars.
      02.06 Closure properties of regular languages and pumping lemma.
      02.07 Regular expressions.
      02.08 Regular expressions and finite-state automata.

03. Context-free languages and pushdown automata:
      03.01 Free grammars and syntax trees.
      03.02 Chomsky normal form.
      03.03 Properties of context-free languages.
      03.04 Pushdown automata and relation with free grammars.
      03.05 Top-down parsing.
      03.06 Bottom-up parsing.

04. Denotational semantics:
      04.01 Denotational semantics for an imperative language.
      04.02 Denotational semantics for an imperative language with blocks and procedures.

05. Operational semantics:
      05.01 Natural semantics for an imperative language.
      05.02 Natural semantics for an imperative language with blocks and procedures.
      05.03 Structural operational semantics for an imperative language.

06. Temporal logics and model checking:
      06.01 Kripke models.
      06.02 Temporal logics.
      06.03 Linear-time logics vs. branching-time logics.
      06.04 Model checking algorithms.

07. Process algebra and behavioral equivalences:
      07.01 Concurrency and nondeterminism.
      07.02 Syntax and semantics of behavioral operators.
      07.03 Trace based equivalence.
      07.04 Bisimulation based equivalence.
      07.05 Test based equivalence.

08. Languages for the specification of software architectures:
      08.01 Components, connectors, and architectural styles.
      08.02 Syntax of an architectural language based on process algebra.
      08.03 Semantics of an architectural language based on process algebra.
      08.04 Behavioral conformity.
      08.05 Topological extensions.

09. Laboratory activity:
      09.01 Specification of software systems through Kripke models.
      09.02 Specification of software systems through architectural languages.
      09.03 Practice on model checking.
      09.04 Practice on equivalence checking.

Programmazione Procedurale e Logica, Matematica Discreta.

Modalità didattiche

Lezioni teoriche ed esercitazioni guidate in laboratorio, sia in presenza che a distanza.

English version: Theory lectures and laboratory exercises, both face-to-face and on-line.

Obblighi

Sebbene consigliata, la frequenza non è obbligatoria.

English version: Although recommended, course attendance is not mandatory.

Testi di studio

Hopcroft, Motwani, Ullman, "Automi, Linguaggi e Calcolabilità", Addison-Wesley, 2009

Hopcroft, Motwani, Ullman, "Introduction to Automata Theory, Languages, and Computation", Addison-Wesley, 2007).

Nielson, Nielson, "Semantics with Applications: An Appetizer", Springer, 2007

Clarke, Grumberg, Peled, "Model Checking", MIT Press, 1999

Aldini, Bernardo, Corradini, "A Process Algebraic Approach to Software Architecture Design", Springer, 2010

Modalità di
accertamento

Progetto individuale e prova scritta.

English version:Individual project and written exam.

Disabilità e DSA

Le studentesse e gli studenti che hanno registrato la certificazione di disabilità o la certificazione di DSA presso l'Ufficio Inclusione e diritto allo studio, possono chiedere di utilizzare le mappe concettuali (per parole chiave) durante la prova di esame.

A tal fine, è necessario inviare le mappe, due settimane prima dell’appello di esame, alla o al docente del corso, che ne verificherà la coerenza con le indicazioni delle linee guida di ateneo e potrà chiederne la modifica.

L'insegnamento è erogato sia in presenza che a distanza nel Corso di Laurea in Informatica Applicata.

English version: The course is offered both face-to-face and on-line within the Laurea Degree Program in Applied Computer Science.