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

Docente responsabile:    Carla Simone

PROGRAMMA

Obiettivi e contenuti

Il corso fornisce gli elementi di base della specifica di processi concorrenti e delle tecniche di valutazione di proprieta' di buon comportamento

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 di Reti Elementari, Reti Posti e Transizioni, cenni a Reti di Petri Temporizzate ed ad Alto Livello.

Grafi di Raggiungibilita', Calcolo degli Invarianti, definizione e valutazione di proprieta' di buon comportamento.

Modularita',  composizionalita', 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 of concurrent processes specification and of the evaluation of their behavioural 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, Predicate/Transition Nets, basic elements of Timed and High Level Petri Nets.

Reachability Graphs, Invariants Calculus, definition and evaluation of behavioural properties.

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

King of evaluton:

  • 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