> ========================================================================================================= > OBIETTIVI FORMATIVI E RISULTATI DI APPRENDIMENTO ATTESI > I risultati di apprendimento attesi specificano conoscenze (teoriche) > e abilità (pratiche, metodologiche, applicate, ecc.) che lo studente > dovrà acquisire con il corso. Indicare quindi gli scopi specifici che > si prefigge il corso, dettagliando ciò che ci si attende lo studente > “conosca” e “sappia fare” al termine delle lezioni. > Dettaglio OBIETTIVI FORMATIVI E RISULTATI DI APPRENDIMENTO ATTESI I > risultati di apprendimento attesi specificano conoscenze (teoriche) e > abilità (pratiche, metodologiche, applicate, ecc.) che lo studente > dovrà acquisire con il corso. Indicare quindi gli scopi specifici che > si prefigge il corso, dettagliando ciò che ci si attende lo studente > “conosca” e “sappia fare” al termine delle lezioni. NOTA IMPORTANTE: Dall'AA 2020/21 in poi il corso "Formal Methods" è diviso in due moduli consecutivi: Modulo I: "Automated Reasoning" [6CFU, di cui 4.5CFU teoria + 1.5CFU laboratorio] Modulo II: "Formal Verification" [6CFU, di cui 4.5CFU teoria + 1.5CFU laboratorio] che sono rispettivamente mutuati come singoli corsi * Automated Reasoning [6CFU, di cui 4.5CFU teoria + 1.5CFU laboratorio] * Formal Verification [6CFU, di cui 4.5CFU teoria + 1.5CFU laboratorio] dal c.d.l. in Artificial Intelligence Systems. Il primo modulo/corso costituisce prerequisito per il secondo. All'interno di entrambi i moduli/corsi è prevista una parte di laboratorio, per complessivi 3 CFU (1.5 CFU Automated Reasoning + 1.5 CFU Formal Verification) Il primo modulo/corso "Automated Reasoning" comincierà quindi all'inizio del semestre e terminerà a metà semestre, mentre il secondo modulo/corso "Formal Verification" comincierà a metà semestre e terminerà a fine semestre. Modulo I: "Automated Reasoning" [6CFU, di cui 4.5CFU teoria + 1.5CFU laboratorio] Le tecniche di ragionamento (logico) automatico sono ampiamente utilizzate in svariati campi, principalmente in Intelligenza Artificiale --come "motori" di svariati sistemi di ragionamento, inferenza e pianificazione automatica-- e nel campo della specifica e verifica formale si sistemi complessi --come "motori" sopra i quali sono costruiti i principali sistemi di verifica automatica. Il Modulo I "Automated Reasoning" presenta un'introduzione alle principali metodologie e agli strumenti per il ragionamento (logico) automatico. Gli studenti sperimenteranno in laboratorio l'uso di tool di automated reasoning, in particolare ad esempio, SAT o SMT solvers. Al termine del modulo/corso, lo studente: - conoscera` le principali tecniche di automated reasoning - sara` in grado di modellare semplici problemi e risolverli tramite automated reasonin tools, quali ad esempio SAT e SMT solvers. Modulo II: "Formal Verification" [6CFU, di cui 4.5CFU teoria + 1.5CFU laboratorio] I metodi di specifica e verifica formali sono progressivamente usati nello sviluppo di sistemi SW e HW industriali come potenti strumenti per la specifica, la verifica e la ricerca di errori. Le metodologie principali e di maggior successo cadono nella famiglia del "Formal Verification", che utilizzano tecniche di automated reasoning come motori. Il Modulo II "Formal Verification" presenta un'introduzione alle principali metodologie e agli strumenti per la specifica e soprattutto la verifica formale di sistemi SW e HW. Il corso si concentrera' sulle tecniche di verifica formale, ed in particolare sulla tecnica "Formal Verification". Gli studenti sperimenteranno in laboratorio l'uso di tecniche di model checking basate sui model checker NuXmv. Al termine del modulo/corso, lo studente: - conoscera` le principali tecniche di specifica e verifica formale, in particolare del Formal Verification - sara` in grado di formalizzare semplici sistemi SW o HW e verificarne proprieta`, tramite il model checker NuXmv. --------------------------------------------------------------------------- IMPORTANT NOTE: Starting from academic year 2020/21, the course "Formal Methods" is split into two consecutive modules: Module I: "Automated Reasoning" [6CFU, of which 4.5CFU theory + 1.5CFU lab] Module II: "Formal Verification" [6CFU, of which 4.5CFU theory + 1.5CFU lab] which are borrowed respectively as single courses * Automated Reasoning [6CFU, of which 4.5CFU theory + 1.5CFU lab] * Formal Verification [6CFU, of which 4.5CFU theory + 1.5CFU lab] from the degree course in Artificial Intelligence Systems. The first module/course is a prerequisite for the second. Part of both modules/courses consists on lab sessions, for 3CFU overall (1.5 CFU Automated Reasoning + 1.5 CFU Formal Verification) As such, the first module/course "Automated Reasoning" will start at the beginning of the semester and end in the middle of the semester, whereas the second module/course "Formal Verification" will start in the middle of the semester and terminate at the end of the semester. Module I: "Automated Reasoning" [6CFU, of which 4.5CFU theory + 1.5CFU lab] Automated (logical) reasoning techniques are widely used in many fields, mainly in Artificial Intelligence --as backend "engines" in several automated reasoning, inference and planning tools-- and in the field of formal specification and validation of complex systems --as backend "engines" on top of which automated-verification tools are build. Module I "Automated Reasoning" introduces the main methodologies and instruments for automated (logical) reasoning. Students will experience in laboratory the usage of automated reasoning tools, in particular, e.g., of SAT and SMT solvers. At the end of the course, the student: - will know the main automated reasoning techniques - will be able to model simple problems and solved them via automated reasoning tools, like e.g. SAT or SMT solvers. Module II: "Formal Verification" [6CFU, of which 4.5CFU theory + 1.5CFU lab] Formal methods are increasingly used as powerful specification, verification and early debugging methods in the development of industrial SW and HW systems. This course provides an introduction to Formal Techniques and Tools for the specification and verification of Hardware and Software platforms. The main and most-successful fall in the "Formal Verification" family, which use automated-reasoning techniques as backend engines. Module II "Formal Verification" introduces the main specification and formal verification techniques of SW and HW devices. The course will concentrate mainly on formal verification and techniques and, in particular, on Formal Verification (FV). A laboratory will be given in which the students will experience MC techniques by means of the MC NuXmv and SPIN. At the end of the course, the student: - will know the main formal specification and verification techniques, in particular Formal Verification - will be able to formalize simple HW and SW systems and verify their properties by means of the model checker NuXmv. > ========================================================================================================= > PREREQUISITI > Indicare le specifiche conoscenze e/o abilità di base che lo studente > deve possedere prima di iniziare il corso > Dettaglio PREREQUISITI Indicare le specifiche conoscenze e/o abilità > di base che lo studente deve possedere prima di iniziare il corso Per entrambi i Moduli "Automated Reasoning" e "Formal Verification": Si assume un minimo background nelle seguenti tematiche: - logica Booleana - algoritmi e strutture dati Un minimo background nelle seguenti tematiche potrà rivelarsi utile: - automi e linguaggi formali - logica del primo ordine --------------------------------------------------------------------------- For both modules "Automated Reasoning" and "Formal Verification": It is assumed some basic background in the following topics: - Boolean logic - basic algorithms and data structures Some background in the following topics could be useful: - automata and formal languages - first-order logic > ========================================================================================================= > CONTENUTI/PROGRAMMA DEL CORSO > Indicare i principali contenuti del corso, nell’ordine temporale con > cui saranno trattati > Dettaglio CONTENUTI/PROGRAMMA DEL CORSO Indicare i principali > contenuti del corso, nell’ordine temporale con cui saranno trattati Per il Modulo I "Automated Reasoning" gli argomenti principali del corso saranno (non necessariamente in ordine): Teoria: * Ragionamento Booleano E Soddisfacibilità Proposizionale (SAT) * Ordered Binary Decision Diagrams * Tecniche moderne di SAT Solving (CDCL) * Funzionalità Estese per SAT * Satisfacibilità Modulo Teorie (SMT) * Funzionalità Estese per SMT * Logiche temporali: LTL, CTL e CTL* * Ragionamento in logica temporale LTL e CTL Laboratorio: * Modellazione e risoluzione di problemi tramite SAT * Modellazione e risoluzione di problemi tramite SMT Per il Modulo II "Formal Verification" gli argomenti principali del corso saranno (non necessariamente in ordine): Teoria: * specifica formale e verifica formale * Rappresentazione Formale di Sistemi * Model Checking (MC): Generalità * Explicit-state MC and Symbolic MC * CTL MC * Fair CTL MC e LTL MC * astrazione in MC * MC per sistemi real-time e ibridi Laboratorio: * modellazione e verifica di sistemi e proprietà con il model checker NuXmv NOTA: Dipendendo da varie circostanze, gli argomenti svolti possono subire variazioni. --------------------------------------------------------------------------- For Module I "Automated Reasoning" the main topics presented in the course are (not necessarily in order): * Boolean Reasoning & Propositional Satisfiability (SAT) * Ordered Binary Decision Diagrams * Modern SAT Solving (CDCL) * Extended SAT Functionalities * Satisfiability Modulo Theories (SMT) * Extended SMT Functionalities * Temporal logics: LTL, CTL and CTL* * Reasoning in Linear Temporal Logic (LTL and CTL) Lab: * Modeling and problem solving via SAT * Modeling and problem solving via SMT For Module II "Formal Verification" the main topics presented are (not necessarily in order): Theory: * Formal specification & formal validation * Formal Representation of Systems * Model Checking (MC): generalities * Explicit-State MC and Symbolic MC * CTL MC * Fair CTL MC and LTL MC * SAT-based MC, * abstraction in MC * MC with Timed and Hybrid Systems Lab: * modeling and verification of systems & properties with the NuXmv model checker NOTE: Depending on various circumstances, the covered topics might be subject to variations. > ========================================================================================================= > METODI DIDATTICI UTILIZZATI E ATTIVITÀ DI APPRENDIMENTO RICHIESTE ALLO > STUDENTE > Indicare: > i metodi didattici e gli strumenti a supporto della didattica che > il docente adotterà per il raggiungimento dei risultati di > apprendimento attesi > le attività di apprendimento che saranno richieste allo studente > > Dettaglio METODI DIDATTICI UTILIZZATI E ATTIVITÀ DI APPRENDIMENTO > RICHIESTE ALLO STUDENTE Indicare: i metodi didattici e gli strumenti a > supporto della didattica che il docente adotterà per il raggiungimento > dei risultati di apprendimento attesile attività di apprendimento che > saranno richieste allo studente Per entrambi i Moduli "Automated Reasoning" e "Formal Verification": Teoria: Le lezioni saranno supportate da slide proiettate via computer, ed integrate da spiegazioni alla lavagna. Agli studenti verrà richiesta padronanza dei concetti teorici, logici ed algoritmici presentati nel corso, e la capacità di rispovere a mano semplici problemi. Laboratorio: Le esercitazioni saranno supportate da slide proiettate via computer, ed integrate da spiegazioni alla lavagna, ed avverranno in aula computer. Agli studenti verrà richiesto di saper modellare sistemi e proprietà nei linguaggi dimacs (SAT), SMT-LIB (SMT), NuXMV (MC), e saperne verificare la correttezza tramite rispettivamente un SAT solver, l'SMT solver MathSAT e il model checker NuXmv. --------------------------------------------------------------------------- For both modules "Automated Reasoning" and "Formal Verification": Theory: The lectures will be supported by computer-projected slides, and integrated by explanations at the board. Students must acquire a deep understanding of the theoretical and algorithmic concepts presented in the course, and the capacity of solving by hand simple formal specification and verification problems. Lab: The lab sessions will be supported by computer-projected slides, and integrated by explanations at the board, and will be held in a computer lab. Student will be required to be able to model systems and properties in the Dimacs (SAT) SMT-LIB (SMT) and NuXMV (MC) languages, and to be able to verify their correctness via some SAT solver, the SMT solver MathSAT, and the NuXMV model checker respectively. > ========================================================================================================= > METODI DI ACCERTAMENTO E CRITERI DI VALUTAZIONE > Indicare: > i metodi di accertamento delle specifiche conoscenze/competenze > acquisite, cioè in cosa consiste la verifica del profitto (se si > tratta di esame scritto/orale, relazione/progetto, se previste > prove in itinere, …) > i criteri utilizzati per la valutazione e i pesi di ogni prova (se > previste prove multiple) > Dettaglio METODI DI ACCERTAMENTO E CRITERI DI VALUTAZIONE Indicare: i > metodi di accertamento delle specifiche conoscenze/competenze > acquisite, cioè in cosa consiste la verifica del profitto (se si > tratta di esame scritto/orale, relazione/progetto, se previste prove > in itinere, …)i criteri utilizzati per la valutazione e i pesi di ogni > prova (se previste prove multiple) Per chi sosterrà l'esame completo di "Formal Methods" (studenti c.d.s. "computer science" o studenti c.d.s "Artificial Intelligence Systems" che intendono sostenere entrambi i moduli in un unico esame) l'esame consistera' in tre prove: 1) un'esercitazione pratica al calcolatore in laboratorio, diretta ad indagare la capacita` dello studente di modellare e risolvere semplici problemi tramite un SAT/SMT solver e formalizzare semplici sistemi SW o HW e verificarne proprieta` tramite il model checkers NuXmv. 2) un test scritto, con un misto di domande a risposta multipla e brevi domande aperte, allo scopo di valutare la conoscenza delle principali tecniche del loro utilizzo. 3) una prova orale sulle tematiche del corso, allo scopo di valutare in dettaglio la conoscenza e padronanza delle tecniche di automated reasoning e specifica e verifica formale, nonche' delle loro motivazioni. Sara` valutata anche la capacita` di esprimere i concetti in modo logico-formale. Le tre parti sono indipendenti, e possono essere superate in appelli diversi, con il vincolo che la prova 3) non puo' essere svolta finche' le prove 1) e 2) non siano entrambe superate. E' necessario conseguire una votazione sufficiente (>= 18/30) in tutte e tre le prove. La votazione finale risultera' da una media pesata delle tre prove, con i seguenti pesi: 1) 20% 2) 30% 3) 50% Per chi vuol sostenere uno o entrambi i moduli singolarmente, per ciascun modulo l'esame consistera' in due prove: 1) Un'esercitazione pratica al calcolatore in laboratorio, diretta ad indagare la capacita` dello studente di modellare e risolvere semplici problemi tramite un SAT/SMT solver [corso "Automated Reasoning"] e formalizzare semplici sistemi SW o HW e verificarne proprieta` tramite il model checkers NuXmv [corso "Formal Verification"]. 2) Un test scritto, con un misto di domande a risposta multipla e brevi domande aperte, allo scopo di valutare la conoscenza delle principali tecniche del loro utilizzo. Le due parti sono indipendenti, e possono essere superate in appelli diversi. E' necessario conseguire una votazione sufficiente (>= 18/30) in entrambe le prove. La votazione finale risultera' da una media pesata delle due prove, con i seguenti pesi: 1) 40% 2) 60% Non sono previste prove in itinere. NOTA: Dipendendo da varie circostanze, le modalità di esame possono subire variazioni, che eventualmente verranno comunicate agli studenti per tempo. --------------------------------------------------------------------------- For those who want to take the complete course exam "Formal Methods" (students c.d.s. "Computer Science" and Students c.d.s "Artificial Intelligence Systems" willing to take both modules in one exam) the exam will consist in three parts: 1) a practical exercise session in computer laboratory, aimed at investigating the capability of the student to model and solve simple problems by means of SAT or SMT solvers, and to formalize simple HW and SW systems and to verify their properties by means of the model checker NuXmv. 2) a script test, with a mix of multiple-answer questions and brief open questions, aimed at evaluating the student knowledge on the main techniques and on their usage. 3) an oral interview on the topics of the course, aimed at evaluating in detail the student knowledge on the main automated reasoning and formal specification and verification techniques and their motivations. The capability of the student of expressing concepts in a formal-logical way will also be evaluated. The three parts are independent and can be passed in different sessions, with the constraint that one cannot try part 3) before passing parts 1) and 2). In order to pass the exam it is necessary to obtain a sufficient grade (>= 18/30) in every part. The final grade will be the weighted average of the grades of the three parts, with the following weights: 1) 20% 2) 30% 3) 50% For those who want to take one of both modules singularly, for each module the exam will consist in two parts: 1) a practical exercise session in computer laboratory, aimed at investigating the capability of the student to model and solve simple problems by means of SAT or SMT solvers ["Automated Reasoning" module], and to formalize simple HW and SW systems and to verify their properties by means of the model checker NuXmv ["Formal Verification" module]. 2) a script test, with a mix of multiple-answer questions and brief open questions, aimed at evaluating the student knowledge on the main techniques and on their usage. In order to pass the exam it is necessary to obtain a sufficient grade (>= 18/30) in every part. The final grade will be the weighted average of the grades of the two parts, with the following weights: 1) 40% 2) 60% Intermediate tests ("prove in itinere") are not envisaged. NOTE: Depending on various circumstances, the exam modalities might be subject to variations, which in case will be communicated to student in due time. > ========================================================================================================= > TESTI DI RIFERIMENTO/BIBLIOGRAFIA > Indicare i testi adottati per lo studio individuale e i materiali > bibliografici adottati > Dettaglio TESTI DI RIFERIMENTO/BIBLIOGRAFIA Indicare i testi adottati > per lo studio individuale e i materiali bibliografici adottati 1) appunti dalle lezioni 2) slides 3) manuali NuXmv e SAT/SMT solvers 4) per il modulo/corso "Automated Reasoning", verranno forniti link ad articoli e tutorials online per il modulo/corso "Formal Verification", uno dei seguenti libri: * Clarke, Grunberg, Long, "Model checking", MIT Press * Baier and Katoen "Principles of Model Checking", MIT Press --------------------------------------------------------------------------- 1) student notes from the classes 2) slides 3) NuXmv e SAT/SMT solvers manuals 4) for the "Automated reasoning" module/course, links to publicly-available articles and tutorials will be provided For the "Formal Verification" module/course, one of the following books: * Clarke, Grunberg, Long, "Model checking", MIT Press * Baier and Katoen "Principles of Model Checking", MIT Press > ========================================================================================================= > ALTRE INFORMAZIONI NOTA IMPORTANTE: Per l'AA 2020/21: per la gestione della pandemia COVID-19, in conformità alle leggi vigenti in materia e in ottemperanza con quanto deciso dalla Consulta dei Direttori e dal Consigli DISI, e a meno di ulteriori decisioni, il corso verrà erogato in modalità "mista" in presenza/in remoto ("blended"): per un numero contingentato di studenti, sarà possibile seguire in aula, secondo i protocolli di sicurezza indicati dall'ateneo, mentre per tutti sarà possibile seguire le lezioni in remoto in modalità sincrona. Il docente si riserva il diritto di decidere di passare alla modalità in remoto qualora valutasse che lo svolgimento delle lezioni in modalità "mista" possa mettere in pericolo la salute degli studenti. Le lezioni saranno comunque videoregistrate e le registrazioni saranno rese disponibili sul sito del corso. --------------------------------------------------------------------------- IMPORTANT NOTE: For academic year 2020/21: due to the handling of the COVID-19 pandemy, in compliance with the current legislation and decisions of the University and Department Councils, and modulo further different decisions, the course classes will be taken in "mixed" remote/in presence modality (a.k.a. "blended"): for a restricted number of students it will be possible to follow the class physically in the classroom --following the access protocols decided by the university-- whereas for everybody it will be possible to follow the classes remotely in synchronous modality. The teacher reserves the right of deciding to switch to the remote modality if he thinks that this is needed for the safety of students. The classes will be video-recorded and the recording files will be made available from the course web site.