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

INSEGNAMENTO: Laboratorio di metodi formali

 

Obiettivi e 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. Acquisizione delle nozioni di base sulle tecniche e sui metodi formali per l'analisi statica e dinamica di codice.

 

Programma esteso

1. Modelli di sistemi concorrenti a eventi discreti e rappresentazioni concrete.

2. Algoritmi e strutture dati per le reti di Petri.

3. Logiche temporali e modali per specificare proprietà dei sistemi.

3. Panoramica di strumenti software per il disegno, l'analisi e la simulazione di modelli di sistemi concorrenti.

4. Cenni a tecniche e metodi per l'analisi statica e dinamica di codice.

 

Risultati di apprendimento previsti

Capacità di progettare e usare strumenti software per il disegno e l'analisi di sistemi concorrenti a eventi discreti; capacità di usare strumenti software per l'analisi statica e dinamica di codice.

 

Prerequisiti

Nozioni fondamentali sulla modellazione di sistemi concorrenti e sulle reti di Petri. Nozioni fondamentali relative all'analisi statica e dinamica di codice.

 

Testi di riferimento:

1. C. Cassandras and S. Lafortune, Introduction to discrete event systems, Kluwer Academic Publishers (capitolo 1)

2. Dispense

Altre informazioni:

 

Tipo esame:

•          Orale

 

 

Course name: Formal methods - laboratory

 

Aims and content: study of 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. Basic notions about techniques and formal methods for static and dynamic analysis of code.

 

Programme

1. Models of concurrent, discrete event systems.

2. Algorithms and data structures for Petri nets.

3. Temporal and modal logics for specifying properties of systems.

3. Sample of software tools for designing, analyzing and executing models of concurrent systems.

4. Techniques and methods for static and dynamic analysis of code.

 

Expected results

Ability to design and using software tools for designing and analyzing discrete event, concurrent systems; ability to use formal methods and software tools for analyzing code.

 

Prerequisites

Basic notions about modelling concurrent systems and Petri nets. Basic notions about static and dynamic analysis of code.

 

References:

1. C. Cassandras and S. Lafortune, Introduction to discrete event systems, Kluwer Academic Publishers (chapter 1)

2. Handouts and notes.

 

Exam:

•          Oral examination

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