Page begin -
Logo DISCO
|
Go to the Highly accessible area
|
Go to the Content page
|
Go to the End of content
|
Go to the Main menu
|
Go to the Navigation Bar (location)
|
Go to the Navigation menu (tree)
|
Go to the Commands list
|
Go to the Further readings
|
Go to the Bottom Menu
|
Logo Ateneo
   
Education
Metodi formali

Codice insegnamento E3101Q018

Docente responsabile: 
Luca Bernardinello

PROGRAMMA

Obiettivi e contenuti:

Il corso fornisce gli elementi di base della specifica di processi concorrenti e delle tecniche di valutazione di proprietà strutturali e dinamiche

Programma:

  • Motivazioni per la specifica formale di processi concorrenti: specifiche eseguibili, controllo distribuito, strumenti di supporto alla progettazione.
  • Classi di reti di Petri con  potenza espressiva crescente: sistemi elementari, reti di posti e transizioni, reti colorate, cenni a reti di Petri stocastiche.
  • Grafi di raggiungibilità, calcolo degli invarianti.
  • Formule e logiche per specificare proprietà, cenni al model-checking.
  • Modularità,  composizionalità, nozioni di equivalenza e di raffinamento.

Risultati di apprendimento previsti:
Gli studenti saranno in grado di affrontare la specifica di piccoli sistemi concorrenti/distribuiti usando i formalismi proposti e le relative tecniche di verifica.

Prerequisiti:

Concetti di base di algebra e di progettazione del software.

Tipo esame:
Scritto e orale

Tipo valutazione
:
Voto finale

 

==============================================
Aims and contents:

The course provides the students with the basic elements for specifying concurrent processes and evaluating their structural and dynamic properties.

Program details:

  • Motivations of concurrent processes formal specification: executable specifications, distributed control, tools supporting design.
  • Classes of Petri nets with increasing expressive power: Elementary Net Systems, Place/Transition Nets, Colored Nets, basics of Stochastic Nets.
  • Reachability Graphs, computation of invariants.
  • Logic formulas for specifying properties, basics of model-checking.
  • Modularity, compositionality, notions of equivalence and refinement.

Learning outcomes:
The students are able to specify small size concurrent/distributed processes using the proposed formalisms and the related verification techniques.

Prerequisites:

Basic notions of algebra and software specification.

Kind of exam:

Written and oral

Kind of evaluation:

Final score

Further readings
(C) Copyright 2016 - Dipartimento Informatica Sistemistica e Comunicazione - Viale Sarca, 336
20126 Milano - Edificio U14
redazioneweb@disco.unimib.it - last update of this page 11/11/2013