Università degli Studi di Urbino Carlo Bo / Portale Web di Ateneo


MODELLAZIONE E VERIFICA DI SISTEMI SOFTWARE
MODELING AND VERIFICATION OF SOFTWARE SYSTEMS

Modellazione e Verifica di Sistemi Software
Modeling and Verification of Software Systems

A.A. CFU
2014/2015 12
Docente Email Ricevimento studenti
Alessandro Aldini mercoledì 10:00-13:00

Assegnato al Corso di Studio

Giorno Orario Aula

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.

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.

Eventuali Propedeuticità

Non vi sono propedeuticità obbligatorie.
 
Si suggerisce di sostenere l'esame di Modellazione e Verifica di Sistemi Software dopo aver sostenuto gli esami di Programmazione Procedurale e Logica, Architettura degli Elaboratori, Matematica Discreta.

Modalità Didattiche, Obblighi, Testi di Studio e Modalità di Accertamento

Modalità didattiche

Lezioni teoriche ed esercitazioni guidate in laboratorio.

Obblighi

Sebbene consigliata, la frequenza non è obbligatoria.

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, prova scritta e prova orale. Il progetto va consegnato almeno due giorni prima della data della prova scritta e pesa per un terzo del voto complessivo. La prova scritta pesa per due terzi del voto complessivo. L'orale è obbligatorio sul progetto e facoltativo sul programma del corso. L'orale facoltativo comporta un aggiustamento positivo o negativo del voto complessivo.

Note

Il corso è erogato sia nel "percorso in presenza" che nel "percorso online" del Corso di Laurea di Informatica Applicata.
Per materiale didattico e informazioni aggiuntive visitare http://www.sti.uniurb.it/aldini/

« torna indietro Ultimo aggiornamento: 23/10/13


Condividi


Questo contenuto ha risposto alla tua domanda?


Il tuo feedback è importante

Raccontaci la tua esperienza e aiutaci a migliorare questa pagina.

Il tuo 5x1000 per sostenere le attività di ricerca

L'Università di Urbino destina tutte le risorse che deriveranno da questa iniziativa alla ricerca scientifica ed al sostegno di giovani ricercatori.

Numero Verde

800 46 24 46

Richiesta informazioni

informazioni@uniurb.it

Posta elettronica certificata

amministrazione@uniurb.legalmail.it

Social

Performance della pagina

Università degli Studi di Urbino Carlo Bo
Via Aurelio Saffi, 2 – 61029 Urbino PU – IT
Partita IVA 00448830414 – Codice Fiscale 82002850418
2019 © Tutti i diritti sono riservati

Top