====== Systems Verification Lab ====== ---- ===== News ===== The course starts on Wed 2nd March 2022 at 2.00 pm in Room AB1 of Polo Lodovici, Building A ---- ===== General Info ===== **Teacher**: * [[http://docenti.unicam.it/pdett.aspx?ids=N&tv=d&UteId=572&ru=RU|Luca Tesei]] **ESSE3 Link** * [[https://didattica.unicam.it/Guide/PaginaADErogata.do?ad_er_id=2021*N0*N0*S2*16873*9988&ANNO_ACCADEMICO=2021&mostra_percorsi=S|Systems Verification Lab - AY 2021/2022]] **Lectures schedule**: * From March 2nd 2022 - Wednesdays from 2.00pm to 4.00pm - Fridays from 11.00am to 1.00pm - Room AB1 of Polo Lodovici **Recording of Lectures and other material**: * The recordings of lectures and the material (slides, codes and exercises) will be given on the **Google Classroom** platform: [[https://classroom.google.com/c/NDU5OTY0NjM2MTE2?cjc=6meqjg2]] (login with @studenti.unicam.it credentials) **Webex Room for Lecture Streaming** * [[http://unicam.webex.com/meet/luca.tesei/|Luca Tesei's room]] **Office hours**: * Take an appointment with the teacher via email. Office hours can be online (webex) or in presence. **Acronym**: * The course official acronym is **SVL2122** ---- ===== Course Objectives ===== See [[https://didattica.unicam.it/Guide/PaginaADErogata.do?ad_er_id=2021*N0*N0*S2*16873*9988&ANNO_ACCADEMICO=2021&mostra_percorsi=S|ESSE3 link]]. ---- ===== Course Contents ===== See [[https://didattica.unicam.it/Guide/PaginaADErogata.do?ad_er_id=2021*N0*N0*S2*16873*9988&ANNO_ACCADEMICO=2021&mostra_percorsi=S|ESSE3 link]]. ---- ===== Lectures ===== * The recordings and other material will be given on the **Google Classroom** platform: [[https://classroom.google.com/c/NDU5OTY0NjM2MTE2?cjc=6meqjg2]] (login with @studenti.unicam.it credentials) ---- ===== Material ===== ==== Textbooks ==== * Christel Baier, Joost-Pieter Katoen, "Principles of Model Checking", The MIT Press, 2008. * Gerard J. Holzmann, "The SPIN model checker: Primer and Reference Manual", Addison-Wesley Professional, 2003. **Reference books** * Michael Huth, Mark Ryan, "Logic in Computer Science", Second Edition, Cambridge University Press, 2004. ISBN: 9780521543101. * Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba, "Reactive Systems", Cambridge University Press, 2007. ==== Verification Tools Links ==== * [[http://spinroot.com/spin/whatispin.html| SPIN Model Checker]] * [[https://spinroot.com/spin/Doc/SpinTutorial.pdf| Spin Tutorial]] * [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-01.pdf|Introduction to SPIN]] * [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-02.pdf|PROMELA 1]] * [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-03.pdf|PROMELA 2]] * [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-04.pdf|Properties 1]] * [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-05.pdf|Properties 2]] * [[http://didawiki.cli.di.unipi.it/lib/exe/fetch.php/magistraleinformatica/mvs/mvs-spin-06.pdf|Properties 3]] * [[https://code.google.com/archive/p/jspin/downloads|JSpin (Java GUI for Spin) Download Site]] * [[http://www.se.rit.edu/~swen-220/resources/SPIN/jSPIN%20Installation.pdf|JSpin Installation Instructions]] * [[http://www.inf.u-szeged.hu/~gombas/HSRV/jspin-user.pdf|JSpin User Guide]] * [[http://nusmv.fbk.eu/| NuSMV Model Cheker]] * [[http://nusmv.fbk.eu/courses/icaps03/icaps03-mct.pdf|NuSMV Slides (together with generic introduction to model checking)]] * [[http://nusmv.fbk.eu/gnusmv/|gNuSMV, GUI for NuSMV]] * [[http://nusmv.fbk.eu/gnusmv/dload/unix/README-linux.html|gNuSVM Linux installation instructions]], [[http://nusmv.fbk.eu/gnusmv/dload/unix/?C=N;O=D|gNuSMV Linux installation files]] * [[http://nusmv.fbk.eu/gnusmv/dload/win32/README_win32.html|gNuSMV Windows installation instructions and files]] * [[https://www.mcrl2.org/web/user_manual/index.html|mCRL2]] * [[http://www.uppaal.org/| UPPAAL Model Checker]] * [[http://www.prismmodelchecker.org/| PRISM Model Checker]] * Other Model Checkers for Timed CTL: * [[https://www-verimag.imag.fr/DIST-TOOLS/TEMPO/kronos/index-english.html|KRONOS Model Checker]] * [[https://sourceforge.net/projects/redlib/|RED Model Checker]] ==== Slides, Codes and Exercises ==== All this material is accessible through the **Google Classroom** platform: [[https://classroom.google.com/c/NDU5OTY0NjM2MTE2?cjc=6meqjg2]] (login with @studenti.unicam.it credentials) ---- ===== Project ===== * The project for 2020/2021 will be given on the **Google Classroom** platform during the course: [[https://classroom.google.com/c/MjkxNDU4MTYwNjA5?cjc=557nyk5]] (login with @studenti.unicam.it credentials) ---- ===== Exams ===== **Exam Dates A.Y. 2021/2022** Dates of Partial Exams "SVL2122 Sess. XXX - Project Delivery" and "SVL2122 Sess. XXX - Written Test" can be found in the [[https://didattica.unicam.it|ESSE3 Career System]] after login. **Exam rules** The exam consists of a written test, containing open-answer questions, together with one project, realised with the tools introduced in the course (see section "Projects" above). The Written Test and the Project are two independent Partial Exams (see the exam sessions in the ESSE3 career system) and can be passed in different exam sessions. The final grade, which is the average of the grades of the two Partial Exams, can be obtained and registered only if both the Partial Exams have been passed with a grade of at least 18/30. **Registration for the written tests** must be done using the Student Career System ESSE3 [[https://didattica.unicam.it|here]]. Please note that the registration **deadline** is usually **3 working days before** the written test date. During the exercise sessions throughout the course samples of the written test questions will be presented with solutions. **During the written test students can consult a hand-written A4 paper of their production for reference.** **Instructions for Sending Projects** Instructions will be part of the Track of the project. ** Exam Results ** * The results will be communicated through this site or by email (depending on the number of students). * Contextually to the communication of the results, students will be invited to accept or reject the evaluation. * A positive evaluation (>=18/30) of each Partial Exam (Written Test and Project) remains valid for **one year** or **until the student retries** the Partial Exam. * If both grades (Written Test and Project) are accepted, the final grade will be registered in ESSE3. ----