Vai al contenuto principale
Oggetto:
Oggetto:

Verifica dei Programmi Concorrenti

Oggetto:

Software Reliability Methods

Oggetto:

Anno accademico 2022/2023

Codice dell'attività didattica
MFN0959
Docenti
Gianfranco Ciardo (Titolare)
Susanna Donatelli (Titolare)
Corso di studi
[008515] Laurea magistrale in informatica
Anno
1° anno 2° anno
Periodo didattico
Secondo semestre
Tipologia
Caratterizzante
Crediti/Valenza
9 CFU - Numero di ore - Number of hours: 56 (in aula) + 16 (in laboratorio)
SSD dell'attività didattica
INF/01 - informatica
Modalità di erogazione
Tradizionale
Lingua di insegnamento
Italiano
Modalità di frequenza
Facoltativa
Tipologia d'esame
Orale
Prerequisiti

Competenze e conoscenze della laurea L31 (Informatica), con particolare attenzione alla capacita' di astrazione e alla conoscenza dei principi di base della concorrenza.
Insegnamenti propedeutici (forniscono le competenze attese in ingresso): Corso di base su linguaggi formali e sistemi operativi (parte sui processi e sulla comunicazione). Il corso di MCAD (modelli concorrenti e algoritmi distribuiti) non è propedeutico, ma lo studente/studentessa che segua entrambi i corsi potrà sicuramente avere una migliore visione di insieme degli argomenti dei due corsi.
Competences and knowledge as acquired through a L-31 curricula. Special requirements are familiarity with abstraction and basic concurrency principles
Preparatory courses (providing the expected entry skills): Basic course on formal languages and basic course on operating system (at least on the topics related to interprocess communication). The MCAD course (Concurrency models and distributed algorithms) is not required, but student can surely acquire a broader knowledge on the course topic by taking also the MCAD course .

Oggetto:

Sommario insegnamento

Oggetto:

Obiettivi formativi

Obiettivo dell'insegnamento e' di fornire gli strumenti, teorici e pratici, necessari alla verifica dei sistemi, ed in particolare del software. Per raggiungere tale obiettivo studieremo alcuni paradigmi di base per la specifica di processi distribuiti, focalizzando l'attenzione sulle capacità modellistiche e sugli strumenti di verifica di proprietà di buon comportamento. Studieremo inoltre la verifica dei sistemi in cui il corretto funzionamento dipende da caratteristiche di tempo. In particolare l'insegnamento ha come obiettivo di far acquisire le competenze teoriche legate ai modelli della concorrenza e di farle applicare per risolvere problemi concreti di verifica del software. Questi obiettivi concorrono al raggiungimento degli obiettivi della laurea magistrale in Informatica, in particolare per quanto riguarda lo sviluppo e la gestione dei  progetti informatici di sistemi complessi e distribuiti e la loro modellazione ed analisi.

This is a course on system verification, with special emphasis on software verification and with a blend of theoretical and applicative issues, all supported by first-hand-experience on "almost real" verification tools. The course aims at providing the theoretical and practical instruments as required for system verification, with special emphasis on software verification. To reach this goal we shall investigate basic modelling languages for distributed systems, as Petri nets and process Algebras, and standard temporal logics for the definition of system properties. We shall extend the study also to timed system, to investigate systems in which correctness is strictly related to the timing aspects of the system. A specific objective of the course is to acquire the theoretical competences in the field of modelling concurrent systems, applied to solving concrete problems of software verification.  The course objectives contribute to the Laurea Magistrale in Informatica overall objectives, in particular for what concerns  the competences in developing and analyzing complex  comples and possibly distributed systems. 

.

 

Oggetto:

Risultati dell'apprendimento attesi

Gli studenti e le studentesse saranno in grado di specificare sistemi concorrenti usando linguaggi formali e di utilizzare strumenti software per la verifica di proprieta' del sistema tramite verifica di proprieta' del modello. In particolare lo studente acquisirà famigliarità con i seguenti strumenti: GreatSPN e NuSMV. Oltre alle classiche proprieta' dei sistemi distribuiti quali assenza di deadlock, fairness e liveness, lo studente sara' in grado di definire e verificare proprieta' in logica temporale quali ad esempio: "se il processo P manda un messaggio, allora non inviera' il prossimo messaggio sino a che non riceve un acknowledgment".

CONOSCENZA E CAPACITÀ DI COMPRENSIONE
Gli studenti e le studentesse saranno in grado di specificare sistemi concorrenti usando linguaggi formali e di utilizzare strumenti software per la verifica di proprieta' del sistema tramite verifica di proprieta' del modello.

CAPACITÀ DI APPLICARE CONOSCENZA E COMPRENSIONE
Gli studenti e le studentesse acquisiranno familiarità con i seguenti strumenti: GreatSPN, NuSMV e Uppaal. Oltre alle classiche proprieta' dei sistemi distribuiti quali assenza di deadlock, fairness e liveness, lo studente sara' in grado di definire e verificare proprieta' in logica temporale quali ad esempio: "se il processo P manda un messaggio, allora non inviera' il prossimo messaggio sino a che non riceve un acknowledgment", oppure "se il processo P manda un messaggio, ricevera' un acknowledge entro 5 unita' di tempo"

AUTONOMIA DI GIUDIZIO
L'acquisizione di autonomia di giudizio è  incrementata grazie alla parte progettuale del corso, in cui viene richiesto di progettare esperimenti e valutarli in modo critico.

ABILITÀ COMUNICATIVE
L'insegnamento prevede un continuo scambio di idee con il docente, in particolare per lo svolgimento dei laboratori, inoltre gli studenti e le studentesse devono preparare una relazione  per ogni laboratorio assegnato.

CAPACITÀ DI APPRENDIMENTO
La preparazione dell'esame prevede la lettura di articoli scientifici (divilgativi) e di due differenti libri di testo. Nell'uso di questi testi sono guidati dal docente, al fine di acquisire le capacità  necessarie a ricercare in modo autonomo risposte sui temi dell'insegnamento.

KNOWLEDGE AND UNDERSTANDING
Having taken this course the student shall be able to specify concurrent systems using formal languages and to apply the associated verification metjods for assessing formally specified system properties

The teaching methodology is aimed at improving in the students the ability of learning in an autonomous manner (reading of scientific reports), of writing reports (written report for the lab assignment) edevelopment of autonoumous judgement (the lab assignment requires the students to organized experiments and evaluate their results). The course objective contribute to the Laurea Magistrale in Informatica overall objectives, in particular for what concerns  the competences in developing and analyzing complex  comples and possibly distributed systems. 

APPLYING KNOWLEDGE AND UNDERSTANDING
Student will be familiar with verification tools like GreatSPN, NuSMV and Uppaal. They shall be able to specify and verify classic properties like absence of deadlock, fairness and liveness, as well as properties specified as temporal logic formulae as, for example: "if a process P sends a message, then it will not send the next message until an acknoledgement of the previous message has been received" or "if a process P sends a message, then it will receive an acknowledge within 5 time units"

INDEPENDENT JUDGEMENT
The lab assignments require the student to set-up experiments and evaluate the obtained results in a critical manner

COMMUNICATION SKILLS
There are frequent cexchange of ideas among the students and between students and teacher. The labs assignment require the student to prepare a (self-contained) written.

LEARNING SKILLS
To prepare for the exam the student should read various scientific papers (meant for the general public) and the use of two different textbooks. Students are guided by teh teacher in the use of these different sources of knowledge, so as to acquire autonomy in learning.

Oggetto:

Modalità di insegnamento

Lezioni frontali, con utilizzo di strumenti di verifica da parte del docente. Le lezioni saranno tenute di persona. Durante il corso vengono assegnati esercizi e mini progetti che gli studenti sono invitati a svolgere durante il corso. Gli esercizi non sono parte della valutazione, ma vengono discussi in classe. Almeno 16 ore vengono dedicate a lezioni/laboratorio in cui vengono presentati gli strumenti di verifica e vengono discussi i problemi che gli studenti hanno incontrato nello svolgimento dei mini progetti. In queste lezioni gli studenti sono invitati a presentare le loro soluzioni che vengono discusse dal docente e dagli altri studenti. Quest'anno l'insegnamento vedrà il contributo di un Visiting Professor, il prof. Gianfranco Ciardo della Iowa State University (USA).

Standard classes with the teacher  using transparencies, blackboard and verification tools "live".  During the course there will be ssmall assignments (not part of the final grade but discussed in class). At least 16 hours of the course are devoted to lab classes during which the students  use the verification tools on small examples or on the assigned exercises.  Students are invited to present their our solution for public discussion. This year the course wil host, as visiting professor,   prof. Gianfranco Ciardo of the Iowa State University (USA).

Oggetto:

Modalità di verifica dell'apprendimento

L'insegnamento ha due modalità di esame, a scelta dello studente/studentessa, a seconda che egli/ella voglia approfondire maggiormente gli obiettivi formativi legati agli aspetti di definizione e confronto dei paradigmi di modellazione concorrente o gli aspetti legati agli strumenti di verifica. Tipo 1: esame orale su argomenti di base del corso e un set esteso di esercizi di laboratorio da discutere con il docente Tipo 2: esame orale su tutti gli argomenti del corso e un insieme ridotto di esercizi di laboratorio da discutere con il docente Per l'esame di tipo 1 la valutazione è basata per il 70% sul laboratorio, ma è comunque richiesta la sufficienza anche nella parte di esame orale per poter superare l'esame. Per l'esame di tipo 2 la valutazione è basata per il 70% sull'orale, ma è comunque richiesta la sufficienza anche nella parte di laboratorio per poter superare l'esame. L'individuazione degli argomenti di base per l'esame di tipo 1 avviene durante il corso, alla fine di ogni macro argomento e viene pubblicato sul sito moodle del corso. Gli esercizi di laboratorio vengono assegnati durante il corso (nella forma "lunga" per l'esame di tipo 1, e nella forma "corta" per l'esame di tipo 2). Gli esercizi sono resi disponibili sul sito moodle del corso.

There are two exam modalities. Each student may choose the preferred form depending on whether they want to learn more on the formal methods or on the associated tools.

Type 1: oral exams on the basic topics of the course (specified on the moodle page of the course)and a full set of lab exercises.  Evaluation: 30-70

Type 2: oral exam on all the topics of the course and a reduced set of lab exercises.  Evaluation 70-30

Topics and lab assignments are all published on the moodle site of the course.

Oggetto:

Attività di supporto

Orari di ricevimento e appuntamenti a richiesta (anche da remoto, se necessario)

Office hours and appointments on request (also on-line if necessary)

Oggetto:

Programma

  • Introduzione alla verifica dei sistemi
  • Un primo linguaggio di specifica, le Reti di Petri (reti posto transizione e reti colorate): definizione, proprieta' e tool disponibili (GreatSPN).
  • Un secondo linguaggio di specifica, le algebre dei processi: definizione, proprieta' di CCS e CSP
  • Un terzo linguaggio di specifica: il linguaggio a guardie del tool NuSMV;
  • Esprimere proprieta': le logiche temporali lineari (LTL) e branching (CTL) e i relativi tool (NuSMV e GreatSPN)
  • Tecniche di analisi per la  verifica di proprietà
  • Esprimere il tempo: gli automi temporizzati, le logiche branching temporizzate e relativi tool (Uppaal)

Topics covered by the course are:

  • an introduction to system verification
  • a first specification language: Petri nets and colored Petri nets; definition, properties and avaiable tools (GreatSPN)
  • a second specification language: process algebras;
  • a third specification language: the guarded commands language of the NuSMV tool;
  • properties' specification languages: linear temporal logic, branching temporal logics and available model-checking tools and associated tools (nuSMV and GreatSPN)
  • Analysis techniques for system properties verification
  • expressing timed models and timed properties: timed automata and timed branching logics and associated tool (Uppaal)

 

 

Testi consigliati e bibliografia



Oggetto:
Libro
Titolo:  
Software Reliability Methods
Anno pubblicazione:  
2001
Editore:  
Springer New York, NY
Autore:  
Doron A. Peled
ISBN  
Permalink:  
Capitoli:  
Introduction, Preliminaries, Modelling Software systems, Formal Specification
Obbligatorio:  
No


Oggetto:
Libro
Titolo:  
Principles of Model Checking
Anno pubblicazione:  
2008
Editore:  
MIT Press
Autore:  
Christel Baier and Joost-Pieter Katoen
ISBN  
Permalink:  
Capitoli:  
Cap. 1, 5, 6, 7.1,9 e Appendix A
Obbligatorio:  
Si
Oggetto:

 


Sul sito moodle viene distribuito del materiale, non coperto da copyright, sulle reti di Petri e le relative tecniche di analisi e sulel algebre di processi. Inoltri  sono indicati link a versione pdf di libri non coperti da copyright e che possono essere di supporto

Students can find on the  moodle site of the course some additional material, not covered by copyright, on Petri nets and process algebra. The moodle page also lists some link to books in  pdf format (books not covered by copyright) that may be useful  to support learning



Oggetto:
Ultimo aggiornamento: 03/05/2023 11:38
Location: https://magistrale.informatica.unito.it/robots.html
Non cliccare qui!