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
Laboratorio di metodi formali

Codice ins.

Insegnamento

CFU ins.

Tipo ins.

Anno

Sem.

SSD ins.

Responsabile insegnamento

E3101Q019

Laboratorio di Metodi Formali

4

OBS

3

2

INF/02

POMELLO Lucia

 

Formal methods – laboratory

 

 

 

 

 

 

Contenuti:
Studio di algoritmi, tecniche e strumenti software per lo sviluppo, la specificazione e l'analisi di modelli di sistemi concorrenti a eventi discreti; più in particolare, strumenti per il disegno e l'analisi di modelli fondati sulle reti di Petri.

Obiettivi formativi:

Capacità di usare strumenti software per il disegno e l'analisi di sistemi concorrenti a eventi discreti; capacità di progettare, sviluppare e integrare semplici funzionalità di alcuni dei precedenti strumenti software.

Prerequisiti:

Nozioni fondamentali sulla modellazione di sistemi concorrenti basati su reti di Petri e sulle proprietà del loro comportamento. (Metodi formali dell’Informatica)

Metodi didattici:

Lezioni ed esercitazioni in aula e in laboratorio, attività di studio e di elaborazione individuale.

 Programma esteso:

  • Modelli di sistemi concorrenti a eventi discreti e rappresentazioni concrete.
  • Algoritmi e strutture dati per le reti di Petri.
  • Specifica e verifica di proprietà di comportamento.
  • Panoramica di strumenti software per il disegno, l'analisi e la simulazione di modelli di sistemi concorrenti.

Testi di riferimento:
Verranno messe  a disposizione dispense e materiale di riferimento.

 Modalità di verifica dell'apprendimento:
Gli studenti dovranno sviluppare un semplice progetto e discuterlo ad un orale.

Tipo esame:
Scritto e orale

Tipo valutazione:
Voto finale

Contents:

Algorithms, techniques, and software tools for specifying, developing and analyzing discrete event system with concurrency; more specifically, tools for designing and analyzing models based on Petri nets.

Aims:
The course aims at developing the ability of  using software tools for designing and analyzing discrete event, concurrent systems; and the ability of developping simple functionalities to be integrated in such tools.

Prerequisites:
Basic notions on modelling concurrent systems and Petri nets (Formal Methods)

Detailed program:

  • Models of concurrent, discrete event systems.
  • Algorithms and data structures for Petri nets.
  • Specification and verification of behavioral properties.
  • Sample of software tools for designing, analyzing and executing models of concurrent systems.

Teaching method:
Lessons and practical exercises, use of laboratories for experimental activities.

Teaching material:
Handouts and notes.

Exam:
The students should develop a simple project to be discussed in a oral examination.

Type of evaluation:
Written and oral

 

 

 

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