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 ins.

Insegnamento

CFU ins.

Tipo ins.

Anno

Sem.

SSD ins.

Responsabile insegnamento

E3101Q018

Metodi formali

4

OBS

3

1

INF/01

BERNARDINELLO Luca

 

Formal methods

 

 

 

 

 

 

Contenuti:
Ruolo e limiti dei metodi formali nella progettazione e nell'analisi del software, particolarmente nel caso di sistemi concorrenti; tecniche per definire la semantica di programmi e sistemi concorrenti; strumenti formali per specificare sistemi concorrenti, i loro requisiti e le loro proprietà.

Obiettivi formativi:
Alla fine del corso lo studente sarà in grado di modellare, a diversi livelli di astrazione, sistemi concorrenti semplici ma non banali e di descriverne i requisiti per mezzo di un linguaggio logico; conoscerà le tecniche per verificarne le proprietà di comportamento.

Prerequisiti:

Metodi didattici
:
Lezioni frontali ed esercitazioni in aula.

Programma esteso:

  •   Natura, applicazioni e limiti dei metodi formali nell'informatica
  •   Sistemi concorrenti e reattivi
  •   Semantiche per sistemi concorrenti
  •   Specificazione di sistemi concorrenti: nozioni generali
  •   Modelli formali di situazioni tipiche nei sistemi concorrenti
  •   Specificazione di sistemi concorrenti: le reti di Petri
  •   Proprietà di comportamento dei sistemi concorrenti: safety e liveness
  •   Logiche modali per esprimere proprietà
  •   Cenni alle tecniche di model-checking

Testi di riferimento:
Dispense e articoli distribuiti durante il corso e publicati sul sito istituzionale.
Modalità di verifica dell'apprendimento:

Tipo esame:
Scritto e orale.

Tipo valutazione:
Voto finale

Content:
Role and scope of formal methods in the design and analysis of software, particularly in the case of concurrent systems; techniques to define the semantics of concurrent programs and systems; formal tools for specifying concurrent systems, requirements, and properties.

Expected achievements:
By the end of the course the student will be able to model, at different levels of abstraction, simple concurrent systems, and to state their requirements with a logical language; s/he will understand the main methods to check behavioural properties of systems.

Detailed topics:

  •   Formal methods in computer science: introductory overview
  •   Concurrent and reactive systems
  •   Semantics for concurrent systems
  •   Specifying concurrent systems: basic notions
  •   Formalized models of typical situations in concurrent systems
  •   Specifying concurrent systems: Petri nets
  •   Safety and liveness properties
  •   Modal logic and properties
  •   Fundamentals of model-checking techniques

Text and materials:
Handouts and papers will be published on the course web site

Exam:
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