====== Systems Verification Lab ====== ---- ===== News ===== * The page of the same course held in Academic Year **2018/2019** can be found at this [[http://didattica.cs.unicam.it/doku.php?id=didattica:magistrale:svl:ay_1819:main|link]]. * **24/09/2019**: The course page is online. * **02/03/2020**: The course officially starts on **Monday 9th March 2020 at 2pm, Room TeamLab**. * **08/03/2020**: The course officially starts on **Monday 9th March 2020 at 2pm, but it will be transmitted only in streaming at the link [[https://unicam.webex.com/meet/luca.tesei]] until, at the moment, the 3rd of April 2020. The timetable is the one specified (Mon 2pm-4pm and Wed 9am-11am). All the lectures will be recorded and made available from the Google Classroom platform, course code 2zjhwud. To join the course, access Google Classroom with the Unicam credentials (@studenti.unicam.it) and subscribe to the course with code: 2zjhwud**. ---- ===== 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=2019*N0*N0*S2*15668*9988&ANNO_ACCADEMICO=2019&mostra_percorsi=S|Systems Verification Lab - AY 2019/2020]] **Lectures schedule**: * Monday 2pm-4pm, Wednesday 9am-11am **Recording of Lectures and other material**: * The links to the recordings of lectures together with other material (besides the slides given in section Material below) will be given through the Google Classroom platform. To join the course, access Google Classroom with the Unicam credentials (@studenti.unicam.it) and subscribe to the course with code: **2zjhwud** **Webex Room for Lecture Streaming** * [[http://unicam.webex.com/meet/luca.tesei/|Luca Tesei's room]] **Office hours**: * Luca Tesei's office hours are specified [[http://docenti.unicam.it/pdett.aspx?ids=N&tv=d&UteId=572&ru=RU|here]], look at the notices for any variation. The place is Luca Tesei's office, 1st floor, Polo Lodovici, via Madonna delle Carceri 9, Camerino. **Acronym**: * The course official acronym is **SVL1920** ---- ===== Course Objectives ===== See [[https://didattica.unicam.it/Guide/PaginaADErogata.do?ad_er_id=2019*N0*N0*S2*15668*9988&ANNO_ACCADEMICO=2019&mostra_percorsi=S|ESSE3 link]]. ---- ===== Course Contents ===== See [[https://didattica.unicam.it/Guide/PaginaADErogata.do?ad_er_id=2019*N0*N0*S2*15668*9988&ANNO_ACCADEMICO=2019&mostra_percorsi=S|ESSE3 link]]. ---- ===== Lectures ===== The links to the recordings of lectures together with other material (besides the slides given in section Material below) will be given through the Google Classroom platform. To join the course, access Google Classroom with the Unicam credentials (@studenti.unicam.it) and subscribe to the course with code: **2zjhwud** * The following links are just for the first lectures. All links will be provided inside the Google Classroom platform. Please, register to the Google Classroom course using your unicam credentials as soon as possible. - Lecture of 09/03/2020 [[https://unicam.webex.com/unicam/ldr.php?RCID=6e79c664e808425dbb0a0d84d86d5b1a|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=e85388cbee6b41adb3d3042da6450701|Download the Lecture]] - Lecture of 11/03/2020 [[https://unicam.webex.com/unicam/ldr.php?RCID=ea94c00b35024a018ba2d4e423ebe3f8|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=f6dadd53d69f4615b151f918d6c2a016|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1920:svl1920-11-03-2020-uppaal-code.zip |UPPAAL Code}} - the subsequent lectures are available only by accessing to the Google Classroom course (see instructions above) ---- ===== Material ===== ==== Verification Tools ==== * [[http://spinroot.com/spin/whatispin.html| SPIN Model Checker]] * [[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]] ==== Reactive Systems ==== **Transition Systems and Modelling Languages for Reactive Systems** * {{ :didattica:magistrale:svl:ay_1920:1_-_introduction_to_model_checking.pdf | Introduction to Model Checking}} * {{ :didattica:magistrale:svl:ay_1920:2_-_transition_systems.pdf |Transition Systems}} * {{ :didattica:magistrale:svl:ay_1920:3_-_modelling_hardware_circuits.pdf |Modelling Hardware Circuits}} * {{ :didattica:magistrale:svl:ay_1920:4_-_program._graphs.pdf |Program Graphs}} * {{ :didattica:magistrale:svl:ay_1920:5_-_guarded_commands_language.pdf |Guarded Command Languages}}, [[https://link.springer.com/chapter/10.1007/978-1-4612-6315-9_14|Original Dijkstra's paper]] * {{ :didattica:magistrale:svl:ay_1920:6_-_parallelism._interleaving_for_ts.pdf |Parallelism: Interleaving for Transition Systems}} * {{ :didattica:magistrale:svl:ay_1920:7_-_parallelism._interleaving_for_program_graphs.pdf |Parallelism: Interleaving for Program Graphs}} * {{ :didattica:magistrale:svl:ay_1920:8_-_parallelism_and_communication._synchronous_message_passing.pdf |Parallelism and Communication: Synchronous Message Passing}} * {{ :didattica:magistrale:svl:ay_1920:9_-_parallelism_and_communication._channel_systems.pdf |Parallelism and Communication: Channel Systems}} * {{ :didattica:magistrale:svl:ay_1920:10_-_parallelism_and_communication._synchronous_product.pdf |Parallelism and Communication: Synchronous Product}} * {{ :didattica:magistrale:svl:ay_1920:11_-_nanopromela_semantics.pdf |Structural Operational Semantics of NanoPROMELA}} **Linear Time Properties** * {{ :didattica:magistrale:svl:ay_1920:1_-_linear_time_properties._introduction.pdf |Introduction to Linear Time Properties}} * {{ :didattica:magistrale:svl:ay_1920:2_-_linear_time_properties._definition_and_satisfaction._trace_equivalence.pdf |Definition and Satisfaction, Trace Equivalence}} * {{ :didattica:magistrale:svl:ay_1920:3_-_linear_time_properties._invariants_and_invariant_checking.pdf |Invariants and Invariant Checking}} * {{ :didattica:magistrale:svl:ay_1920:4_-_linear_time_properties._safety_properties._bad_prefixes_and_prefix_closure.pdf |Safety Properties}} * {{ :didattica:magistrale:svl:ay_1920:5_-_linear_time_properties._liveness_properties.pdf |Liveness Properties}} * {{ :didattica:magistrale:svl:ay_1920:6_-_linear_time_properties._decomposition_theorem.pdf |Decomposition Theorem}} * {{ :didattica:magistrale:svl:ay_1920:linear_time_properties._regular_safety_properties.pdf |Regular Safety Properties}} * {{ :didattica:magistrale:svl:ay_1920:7_-_linear_time_properties._fairness.pdf |Fairness}} **Linear Time Logic (LTL)** * {{ :didattica:magistrale:svl:ay_1920:1_-_ltl_syntax_and_semantics.pdf |Syntax and Semantics of LTL}} * {{ :didattica:magistrale:svl:ay_1920:2_-_ltl_equivalences_and_laws.pdf |Equivalences and Laws of LTL}} * {{ :didattica:magistrale:svl:ay_1920:3_-_ltl_expressing_fairness.pdf |Expressing Fairness in LTL}} **Computation Tree Logic (CTL)** * {{ :didattica:magistrale:svl:ay_1920:1_-_ctl_syntax_semantics_equivalences_and_normal_forms.pdf |Syntax, Semantics, Equivalences and Normal Forms of CTL}} * {{ :didattica:magistrale:svl:ay_1920:2_-_ctl_vs_ltl.pdf |CTL versus LTL}} * {{ :didattica:magistrale:svl:ay_1920:4_-_ctl_with_fairness.pdf |CTL with Fairness}} ==== Timed Systems ==== **Timed Automata** * {{ :didattica:magistrale:svl:ay_1920:1_-_timed_automata.pdf |Timed Automata}} * {{ :didattica:magistrale:svl:ay_1920:2_-_timed_paths_divergence_timelocks_zenoness.pdf |Timed Paths, Divergence, Timelocks, Zenoness}} * {{ :didattica:magistrale:svl:ay_1920:3_-_timed_ctl.pdf |Timed CTL}} * [[http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf|UPPAAL Tutorial]] ==== Probabilistic Systems ==== **Markov Chains** * [[http://www.prismmodelchecker.org/lectures/esslli10/esslli10pmc-part1.pdf|Discrete Time Markov Chains and TCTL]] * [[http://www.prismmodelchecker.org/lectures/esslli10/esslli10pmc-part4.pdf|Probabilistic model checking in practice]] * [[http://www.prismmodelchecker.org/tutorial/|PRISM Tutorial]] * [[http://www.prismmodelchecker.org/manual/Main/Welcome|PRISM Manual]] ==== Exercises ==== **Exercises with (some) solutions** * {{ :didattica:magistrale:svl:ay_1920:exsolmodelsandmodelling.pdf |Transition Systems and Modelling Languages for Reactive Systems}} * {{ :didattica:magistrale:svl:ay_1920:exsollineartime.pdf |Linear Time Properties}} * {{ :didattica:magistrale:svl:ay_1920:exsolltlctl_with_exercises_from_book.pdf |Regular Properties, LTL and CTL}} - **NOTE 1:** some of the exercises on Regular Properties and on LTL require to calculate the product between the transition system and the non-Deterministic Buechi Automaton (NBA) corresponding to the formula - ignore that part and justify your answer by providing the counterexample without providing the product construction. **NOTE 2:** some of the exercises on CTL require to show the steps of the Sat algorithm for deciding the satisfaction of the formula by a state or by a transition system: ignore this request and provide, if possible, an informal justification; if not possible ignore the exercise. ==== Sample Past Written Tests with Solutions ==== * {{ :didattica:magistrale:svl:ay_1920:svl1819appello1.pdf |Text1}}, {{ :didattica:magistrale:svl:ay_1920:svl1819appello1solutionwithnotes.pdf |Text1 with Solutions}} * {{ :didattica:magistrale:svl:ay_1920:svl1819appello2.pdf |Text2}}, {{ :didattica:magistrale:svl:ay_1920:svl1819appello2withsolution.pdf |Text2 with Solutions}} * {{ :didattica:magistrale:svl:ay_1920:svl1819appello3.pdf |Text3}}, {{ :didattica:magistrale:svl:ay_1920:svl1819appello3_with_solutions.pdf |Text3 with Solutions}} * ==== Textbooks ==== Main: * Christel Baier, Joost-Pieter Katoen, “Principles of Model Checking”, The MIT Press, 2008. Reading: * Vidyadhar G. Kulkarni, "Modeling and Analysis of Stochastic Systems, Third Edition", Chapman and Hall/CRC, 2016. **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. ---- ===== Project ===== - The text of the project can be found in the Google Classroom platform. ---- ===== Exams ===== **Exam Dates A.Y. 2019/2020 (Written Test Days)** - For each session, projects can be sent by the day before the written test (see Partial Exams "SVL1920 Sess. XXX - Project Delivery" in ESSE3) - 06/02/2020 - 3pm - Room TBD, please register to the Partial Exam "SVL1920 Sess. I - Written Test" on ESSE3 before 31/01/2020 - 20/02/2020 - 3pm - Room TBD, please register to the Partial Exam "SVL1920 Sess. II - Written Test" on ESSE3 before 14/02/2020 - 25/06/2020 - 3pm - Room TBD, please register to the Partial Exam "SVL1920 Sess. III - Written Test" on ESSE3 before 19/06/2020 - 09/07/2020 - 3pm - Room TBD, please register to the Partial Exam "SVL1920 Sess. IV - Written Test" on ESSE3 before 03/07/2020 - 23/07/2020 - 3pm - Room TBD, please register to the Partial Exam "SVL1920 Sess. V - Written Test" on ESSE3 before 17/07/2020 - 10/09/2020 - 3pm - Room TBD, please register to the Partial Exam "SVL1920 Sess. VI - Written Test" on ESSE3 before 04/09/2020 - 24/09/2020 - 3pm - Room TBD, please register to the Partial Exam "SVL1920 Sess. VII - Written Test" on ESSE3 before 18/09/2020 - 25/03/2021 - 3pm - Room TBD, please register to the Partial Exam "SVL1920 Sess. VIII - Written Test" on ESSE3 before 19/03/2021 For registration, please consult the [[https://didattica.unicam.it|ESSE3 Portal]] 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** Students must create a folder in Google Drive, using the Google account associated to their email name.surname@studenti.unicam.it The folder must contain all the files relative to the project and a written report, in English, which describes all the phases of the developing of the project. The use of screenshots is encouraged to show, within the report, the runs and the results of the project. The folder must be named SVL1920-Project-N-APP-X-Surname-Name where N is the number of the realised project (according to the section "Projects" above) and X is the number of the exam session (Appello) as specified for each date of the written test above. The folder must be shared (using Google Drive facilities) with luca.tesei@unicam.it and andrea.polini@unicam.it by 11.59pm of the day before the written test scheduled for the selected session X. Students that send the project must also register to the Partial Exam "SVL1920 Sess. XXX - Project Delivery" in ESSE3, specified for each exam session. ** 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. ----