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

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