Skip to main content
If you continue browsing this website, you agree to our policies:
  • Condizioni di utilizzo e trattamento dei dati
Continue
x
If you continue browsing this website, you agree to our policies:
  • Condizioni di utilizzo e trattamento dei dati
Continue
x
e-Learning - UNIMIB
  • Home
  • More
Listen to this page using ReadSpeaker
English ‎(en)‎
English ‎(en)‎ Italiano ‎(it)‎
 Log in
e-Learning - UNIMIB
Home
Percorso della pagina
  1. Science
  2. Bachelor Degree
  3. Informatica [E3102Q - E3101Q]
  4. Courses
  5. A.A. 2024-2025
  6. 3rd year
  1. Formal Methods
  2. Summary
Insegnamento Course full name
Formal Methods
Course ID number
2425-3-E3101Q121
Course summary SYLLABUS

Course Syllabus

  • Italiano ‎(it)‎
  • English ‎(en)‎
Export

Obiettivi

In questo corso si considerano sistemi concorrenti o distribuiti costituiti da componenti che operano in modo indipendente e che interagiscono tra loro in diverse modalità. Alla fine del corso lo studente avrà acquisito strumenti di base per modellare, a diversi livelli di astrazione, tali sistemi, per descriverne i requisiti per mezzo di un linguaggio logico; conoscerà le tecniche per verificarne le proprietà di comportamento; saprà usare alcuni strumenti software per il disegno e l'analisi. Tali competenze sono utilizzabili in diversi contesti applicativi come ad esempio la progettazione di software concorrente, dei protocolli di comunicazione, ...

Contenuti sintetici

Viene introdotto un linguaggio logico per specificare le proprietà di comportamento di sistemi concorrenti; vengono presentate le reti di Petri come utile strumento per modellare tali sistemi e analizzarne le proprietà. Vengono introdotti algoritmi e strumenti software per tale modellazione e analisi.

Programma esteso

1. Panoramica dei metodi formali nella progettazione e analisi del software, in particolare nel caso di sistemi concorrenti.

2. Un linguaggio logico per specificare le proprietà di comportamento dei sistemi concorrenti: la logica proposizionale temporale lineare PLTL. Sintassi e semantica, equivalenza tra formule. Esempi di formule PLTL insoddisfacibili. Proprietà di liveness, di safety e di fairness in PLTL Sistemi di transizioni e model checking.

3. Linguaggi e strumenti software per la specifica e analisi dei sistemi e programmi concorrenti

4. Le Reti di Petri: fondamenti concettuali, applicazioni e tecniche di analisi: i sistemi elementari, la regola di scatto e il grafo dei casi raggiungibili. Reti Posti e Transizioni: matrice di incidenza, vettore di Parikh e l’equazione di stato. Proprietà di comportamento e loro verifica sul grafo di raggiugbilità. Analisi strutturale: S- e T-invarianti; sifoni e trappole; teoremi del rango. Sottoclassi particolari: macchine a stati, grafi marcati, reti Free-choice e verifica di proprietà su tali sottoclassi. Altre classi di reti.

Prerequisiti

Nozioni di base di logica proposizionale, nozioni di base di analisi matematica e di matematica discreta (come trattata nel corso di fondamenti dell'nformatica).

Modalità didattica

Il corso è erogato in italiano. Lezioni ed esercitazioni in aula, svolte in modalità erogativa in presenza.
Esercitazioni di laboratorio, svolte in modalità interattiva in presenza.

Materiale didattico

Dispense e articoli monografici forniti dal docente tramite la piattaforma e-learning

Periodo di erogazione dell'insegnamento

Secondo semestre

Modalità di verifica del profitto e valutazione

La verifica dell'apprendimento comprende una prova scritta e un colloquio orale.

Nella prova scritta si richiede di svolgere alcuni esercizi simili a quelli svolti a lezione e durante le esercitazioni e in laboratorio. L'obiettivo di valutazione della prova scritta consiste nel controllo della preparazione su alcuni argomenti fondamentali del programma d’esame, e nel controllo delle competenze di problem solving disciplinare.

Si è ammessi al colloquio orale se è stata superata la prova scritta
Al colloquio orale, oltre alla discussione dello scritto, vengono fatte domande sugli argomenti del corso. L'obiettivo del colloquio orale è valutare la capacità dello studente di esporre gli argomenti del corso, e di effettuare brevi ragionamenti su di essi.

La valutazione è complessiva e viene definita al colloquio orale.

Orario di ricevimento

Su appuntamento.

Sustainable Development Goals

ISTRUZIONE DI QUALITÁ
Export

Aims

We consider concurrent or distributed systems done by components that operate independently and interact with each other in different ways. At the end of the course, the student will have acquired the basic tools to model, at different levels of abstraction, such systems, to describe their requirements by means of a logical language; she/he will know the techniques for verifying system behavioral properties, and will be able to use some software tools for the design and analysis. These skills can be used in various application contexts such as the design of concurrent software, communication protocols, ...

Contents

A logic language will be introduced to specify behavioral properties of concurrent systems. Petri nets will be presented as useful formal tools to model concurrent systems and to analyze their properties. Algorithms and software tools for the design and analysis of such systems will be also introduced.

Detailed program

1. Survey of formal methods in the design and analysis of concurrent systems.

2. A logic language to specify behavioral properties of concurrent systems: Propositional Linear Temporal Logic (PLTL), syntax and semantics, equivalence of formulas, examples of unsatisfiable formulas in PLTL, properties of liveness, safety and fairness in PLTL. Transition systems and model checking.

3. Languages and software tools to specify and analyse concurrent systems and programs.****
4. Petri nets: conceptual foundation, applications, and analysis techniques: elementary net systems, transition rule, case graph. Place Transition nets: incidence matrix, Parikh vector, state equation. Behavioral properties and their verification on the reachability graph. Structural analysis: S- and T-invariants; siphons and traps; rank theorems. Net subclasses: state machines, marked graphs, Free-choice nets and analysis of behavioral properties on such subclasses. Other classes of nets.

Prerequisites

Basic notions of propositional logic, basic notions of mathematical analysis and of discrete mathematics (as presented in the course of Fundamentals of Computer Science).

Teaching form

Language: Italian.
Classroom lessons and exercises, carried out in delivered mode, in person.
Laboratory activity, carried out in interactive mode, in person.

Textbook and teaching resource

Handouts, research and survey papers on the e-learning platform

Semester

Second semester

Assessment method

The assessment method consists of written and oral examination

The written exam consists of some exercises, which are similar to the ones made in class during the lectures.
The evaluation objective of the written test consists in the control of the preparation on some fundamental topics of the exam program, and in the control of disciplinary problem solving skills.

The student is admitted to the oral exam if he/she has passed the written test
In the oral exam the solution of such exercises will be discussed and some questions on the developed arguments will be done.
The objective of the oral interview is to evaluate the student's ability to present the topics of the course, and to make brief thoughts on them.

The assessment is comprehensive and is defined in the oral interview.

Office hours

On appointment

Sustainable Development Goals

QUALITY EDUCATION
Enter

Key information

Field of research
INF/01
ECTS
8
Term
Second semester
Activity type
Mandatory to be chosen
Course Length (Hours)
0
Degree Course Type
Degree Course
Language
Italian

Staff

    Teacher

  • LB
    Luca Bernardinello
  • GF
    Guido Giuseppe Fiorino
  • LP
    Lucia Pomello Chinaglia Pomello

Students' opinion

View previous A.Y. opinion

Bibliography

Find the books for this course in the Library

Enrolment methods

Self enrolment (Student)
Manual enrolments

Sustainable Development Goals

QUALITY EDUCATION - Ensure inclusive and equitable quality education and promote lifelong learning opportunities for all
QUALITY EDUCATION

You are not logged in. (Log in)
Policies
Get the mobile app
Powered by Moodle
© 2025 Università degli Studi di Milano-Bicocca
  • Privacy policy
  • Accessibility
  • Statistics