Inizio della pagina -
Logo DISCO
|
Visita la Versione ad elevata leggibilità
|
Vai al Contenuto della pagina
|
Vai alla Fine dei contenuti
|
Vai al Menu Principale
|
Vai alla Barra di navigazione (sei in)
|
Vai al Menu di navigazione (albero)
|
Vai alla Lista dei comandi
|
Vai alla Lista degli approfondimenti
|
Vai al Menu inferiore
|
Logo Ateneo
   
Per gli Studenti
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

Approfondimenti

Google Translate
Translate to English Translate to French Translate to German Translate to Spanish Translate to Chinese Translate to Portuguese Translate to Arabic
Translate to Albanian Translate to Bulgarian Translate to Croatian Translate to Czech Translate to Danish Translate to Dutch Translate to Finnish Translate to Greek Translate to Hindi
Translate to Hungarian Translate to Irish Translate to Japanese Translate to Korean Translate to Norwegian Translate to Polish Translate to Romanian Translate to Russian Translate to Serbian
Translate to Slovenian Translate to Swedish Translate to Thai Translate to Turkish

(C) Copyright 2016 - Dipartimento Informatica Sistemistica e Comunicazione - Viale Sarca, 336
20126 Milano - Edificio U14
redazioneweb@disco.unimib.it - ultimo aggiornamento di questa pagina 11/11/2013