- Oggetto:
- Oggetto:
Verifica dei Programmi Concorrenti - Parte A
- Oggetto:
Software Reliability Methods - A
- Oggetto:
Anno accademico 2023/2024
- Codice attività didattica
- MFN1360
- Docente
- Susanna Donatelli (Titolare)
- Anno
- 1° anno, 2° anno
- Periodo
- Secondo semestre
- Tipologia
- Caratterizzante
- Crediti/Valenza
- 6 CFU - Numero di ore - Number of hours: 40 (in aula) + 8 (in laboratorio)
- SSD attività didattica
- INF/01 - informatica
- Erogazione
- Tradizionale
- Lingua
- Italiano
- Frequenza
- Facoltativa
- Tipologia esame
- Orale
- Prerequisiti
- Competenze e conoscenze della laurea L31, 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 . - Mutuato da
- Verifica dei Programmi Concorrenti (MFN0959)Corso di laurea magistrale in Informatica
- Verifica dei Programmi Concorrenti (MFN0959)
- Oggetto:
Sommario insegnamento
- Oggetto:
Avvisi
- 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. In particolare il corso 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. Le modalità di insegnamento favoriranno l'acquisizione, da parte degli studenti, di capacità autonoma di apprendimento, (comprensione di articoli scientifici sugli argomenti del corso), di abilità comunicative (relazioni associate agli esercizi di laboratorio e discussioni in classe) e di autonomia di giudizio (grazie a laboratori in cui gli studenti debbono organizzare esperimenti e valutazione delgi stessi. 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 prioviding 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. 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.The student will be able to define specifications of concurrent system by means of formal languages and to exploit software tools for the verification of program properties, via a verification of the model properties. In particular, the student will acquire familiarity with the following tools: GreatSPN e NuSMV. In addition to the classical properties of the distributed systems, such as deadlock absence, fairness e liveness, the student will be able to define and verify properties as, for instance: "if the process P sends a message, then it will not send the next message until it gets an acknowledgment".
KNOWLEDGE AND UNDERSTANDING
The student shall be able to specify concurrent systems using formal languages and to apply the associated verification metjods for assessing formally specified system propertiesThe 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 mannerCOMMUNICATION 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:
Programma
- Introduzione alla verifica dei sistemi
- Un primo linguaggio di specifica, le Reti di Petri (reti posto transizione): definizione, proprieta' e tool disponibili (GreatSPN).
- Un secondo linguaggio di specifica, le algebre dei processi: definizione, proprieta' di CCS e CSP
- Esprimere proprieta': le logiche temporali lineari (LTL) e branching (CTL) e i relativi tool (NuSMV e RGMEDD)
NOTA: rispetto al corso da 9 cfu gli argomenti mancanti sono le reti di Petri colorate (e relativi esercizi) e la parte sul tempo (timed automata e Uppaal)
Topics covered by the course are:- an introduction to system verification
- a first specification language: Petri nets; definition, properties and avaiable tools (GreatSPN)
- a second specification language: process algebras;
- properties' specification languages: linear temporal logic, branching temporal logics and available model-checking tools and associated tools (nuSMV and RGMEDD)
NOTE: with respect to the 9 cfu course, the following subjects are not included: colored Petri Nets (and related exercises) and the temporal part (timed automata e Uppaal).
- 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)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 supportoStudents 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:
