====== Systems Verification Lab ====== ---- ===== News ===== * **26/05/2019**: Project for 2018/2019 is available in the relative section below. * **13/05/2019**: On **Thursday 16/05/2019** there will be **two extra lectures** given as seminars of **Dr. Matteo Rucco**. The first one is scheduled at 11:00am in Room AB1 and the second one is scheduled at 04.30pm in Room AB1 as well. * **07/04/2019**: The calendar of the course has been updated, please take note of the new dates in section "Lectures" below. * **04/04/2019**: The Lecture of **Wednesday 10/04/2019** is **cancelled** because the teacher is in the evaluation committee of Bsc and MSc graduation. * **29/03/2019**: The Lecture of **Wednesday 03/04/2019** will take place in **Room AB1** of Polo Lodovici instead of the usual Room LA1. * **04/03/2019**: From **Monday 11/03/2019** on the lecture of Mondays will be on **Room LA2** of Polo Lodovici. * **04/03/2019**: The course officially starts Monday 04/03/2019 at 2pm in Room AB1 of Polo Lodovici. ---- ===== 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=2018*N0*N0*S2*14679*9988&ANNO_ACCADEMICO=2018&mostra_percorsi=S|Systems Verification Lab - AY 2018/2019]] **Lectures schedule**: * Monday 2pm - 4pm - (from 11/03/2019) Room LA2 of Polo Lodovici * Wednesday 9am - 11am - Room LA1 of Polo Lodovici **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 **SVL1819** ---- ===== Course Objectives ===== **KNOWLEDGE AND UNDERSTANDING** At the end of the course, the student should be able to: - Understand the concept of verification of a concurrent system and the main issues related to the model checking problem of reactive systems - Define the formalism of transitions systems for modelling concurrent systems also using more higher level concepts such as state variables and communication channels - Illustrate the concepts of parallel composition, interleaving, synchronous communication, synchronised product between transition systems - Have knowledge of the type of properties that can be expressed on a trace of a transition system: safety, liveness or mixed properties - Illustrate the concept of fairness of actions - Illustrate the syntax and the semantics of Linear Time Logic (LTL) - Illustrate the syntax and the semantics of Computation Tree Logic (CTL) - Understand the issues related to time critical systems and the need of expanding non-deterministic formalisms with time - Understand the concepts of clock variables, timed automata, timed paths, divergence and zenoness - Illustrate the syntax and the semantics of Timed Computation Tree Logic (TCTL) - Understand the concept of probabilistic and stochastic systems and their verification - Illustrate the definition of Discrete Time Markov Chains (DTMC), Markov Decision Processes (MDP) and Continuous Time Markov Chains (CTMC) - Illustrate the syntax and the semantics of Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL) **APPLYING KNOWLEDGE AND UNDERSTANDING** At the end of the course, the student should be able to: - Model a concurrent reactive system using a component-based approach - Define finite state machines with a suitable synchronisation interface using both a graphical language and a textual language - Formally express properties of reactive systems using LTL and CTL formulas - Apply the concept of fairness to real cases - Use a tool for the model checking of reactive systems - Use the formalism of Timed Automata for modelling real-time systems - Use the tool UPPAAL for verifying real-time systems - Use the formalisms of DTMC, MDP and CTMC for modelling probabilistic or stochastic systems - Use the tool PRISM for verifying probabilistic or stochastic systems **MAKING JUDGEMENTS** At the end of the course, the student should be able to: - Identify the best model suitable for describing a system using a given formalism **COMMUNICATION SKILLS** At the end of the course, the student should be able to: - Write a clear report on the modelling and analysis of a system under study using a formal style **LEARNING SKILLS** At the end of the course, the student should be able to: - Search the scientific literature for specific advances in formalisms and tools aimed at modelling and verifying reactive, real-time, probabilistic and stochastic systems - Autonomously understand and learn to use new features added to tools for modelling and verifying reactive, real-time, probabilistic and stochastic systems ---- ===== Course Contents ===== System verification: main concepts. Definition and characteristics of model checking. Transition Systems. Program Graphs and Channel Systems. Parallelism and communication. The state-space explosion problem. Linear-time properties: safety, liveness, fairness. Linear Temporal Logic (LTL). Computation Tree Logic (CTL). Model checking of reactive systems with a software tool. Real-time systems and timed formalisms. Timed Automata. Timed Computation Tree Logic (TCTL). The UPPAAL Tool. Probabilistic and Stochastic Systems. Discrete Time Markov Chains (DTMC), Markov Decision Processes (MDP) and Continuous Time Markov Chains (CTMC). Probabilistic Computation Tree Logic (PCTL) and Continuous Stochastic Logic (CSL). The tool PRISM. ---- ===== Lectures ===== - 04/03/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=9c885e58219bcc1d480f0408e618f1ff|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=945c59f92b3df9a9ebed8b099a3d1ba9|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:lectureincdecreset.xml.zip |First Example in UPPAAL}} - 06/03/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=ff3cb5baa769a1b410b46f690500323d|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=f0a161129cd8a47fca8c251ba5ea17de|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:uppaalmodels-06-03-2019.zip |UPPAAL Models}} - 11/03/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=adf972e78f841be4f37f55411d1912b6| Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=0e063a181e624474c2c7c686ae1eed60| Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:uppaalmodels-11-03-2019.zip |UPPAAL Models}}, {{ :didattica:magistrale:svl:ay_1819:spinmodels11-03-2019.zip |SPIN Models}}, [[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]] - 13/03/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=4f815cc3ab91808ac706bf9b52618e55|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=46e5a06bc7a64f9aab671a9b616612a0|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:spinmodels-13-03-2019.zip |SPIN Models}} - 18/03/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=b6df8f94ff09850c5b02b46ddaaea877|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=9007c71993f3c65ed703371fa91e9123|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:uppaalmodels-18-03-2019.zip |UPPAAL Models}}, Suggested exercise: model in UPPAAL the supermarket booking system and the train-gate system, {{ :didattica:magistrale:svl:ay_1819:spinmodel-uncompleted-18-03-2019.zip |SPIN Models (Uncompleted)}}, Suggested exercise: complete the specification of the Alternate Bit Protocol in PROMELA. - 20/03/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=dc4afcd063d3f09fb69b433e7f6469dd|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=caff92c09ccac2b2b0e4f6a32f05beb9|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:spinmodels-20-03-2019.zip |SPIN Models (abp)}}, {{ :didattica:magistrale:svl:ay_1819:svl-notes-20-03-2019.pdf |Notes}} - 25/03/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=6ff9d46a1dda85ca45042d52df555d31|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=7af4c80918eb80545e990a3200c5ad09|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:nusmv-models-25-03-2019.zip |NuSMV Models}} - 27/03/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=e21dc3d8f9c5d01567bb698397a87a9b|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=5516ca87061e310a93d59cdb7005088b|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:svl-notes-27-03-2019.pdf |Notes}} - 01/04/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=2ac4f960bea678a364d9ed41e2ca0938|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=1219e1bc393060240cdc63e2cd379ddc|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:svl-notes-01-04-2019.pdf |Notes}} - 03/04/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=58b06a5073151b1c5b2e50b6212bf54f|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=614e6648080b72cc1c92f8913b882f12|Download the Lecture]] - 08/04/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=ae7e771b6b7bfd760b388c4410271c78|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=af2d66d36461bb27cf011998462034d1|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:svl-notes-08-04-2019.pdf |Notes}} - 29/04/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=8eee88ea6bd890f1832480f808b94198|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=54ff1e1d9b12c729d37f2220c40c21e8|Download the Lecture]] - 06/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=7c81597de48f5d02dab5eff48627f43b|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=5ac277d81da17bf5eaec0018e0f944bb|Download the Lecture]] - 08/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=1d452fa7c419f6e56c755fb8bd7d02ec|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=88fe3e310fcd3a6dc83acb890ea108fe|Download the Lecture]] - 13/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=fa20cf5354e395670fc4d9be7bf96c25|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=9f5cbc0c2efb146c892509f8db2e45a0|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:svl-notes-13-05-2019.pdf |Notes}}, [[http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf|UPPAAL Tutorial]] - 15/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=d31f0c044e2b798205b5c7c03e164637|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=5db1a79662b0bde33a1b643a17d5254a|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:svl-notes-15-05-2019.pdf |Notes}}, [[https://www.youtube.com/watch?v=skM37PcZmWE|Achilles and the Tortoise]] - 16/05/2019 - **Seminar Lectures** of Matteo Rucco: {{ :didattica:magistrale:svl:ay_1819:locandina_per_seminari_logo_unicam_matteo_rucco_1.pdf |Seminar 1}}, {{ :didattica:magistrale:svl:ay_1819:locandina_per_seminari_logo_unicam_matteo_rucco_2.pdf |Seminar 2}} - 20/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=757d010998a9781d6cb8845c3fb664a2|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=79a1b8e3d1ac3e7e369bd8c1af2066b6|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:traingatetimed.xml.zip |UPPAAL Model}} - 22/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=bf66275e77194d5a7fbf26474fb3713c|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=99f0ba434e2ae527efb097ecea23c1f0|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:svl1819-uppaalcode-22-05-2019.zip |UPPAAL Models}}, [[http://www.prismmodelchecker.org/lectures/esslli10/esslli10pmc-part1.pdf|PRISM Slides on DTMCs]] - 27/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=fd2024522f965a22d558e4f5e264d1c5|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=88b6f1506cef838aa5d6b7912dcf3c47|Download the Lecture]], [[http://www.prismmodelchecker.org/lectures/esslli10/esslli10pmc-part1.pdf|PRISM Slides on DTMCs]], {{ :didattica:magistrale:svl:ay_1819:die.zip |Die example in PRISM}} - 29/05/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=2002b01720dd0c5a47db5c5e58078523|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=659b29de0a5729945b0e52aac477c53c|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:herman7.zip |PRISM Code}}, [[http://www.prismmodelchecker.org/lectures/pmc/03-dtmcs.pdf|Slides Long-run Probability]], {{ :didattica:magistrale:svl:ay_1819:svl-notes-29-05-2019.pdf |Notes}} - 03/06/2019 - [[https://unicam.webex.com/unicam/ldr.php?RCID=8ab1c9d51279cda185dc64b5fad97ce9|Watch the Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=e9720bd0c38830e0065c222d2c20a62f|Download the Lecture]], {{ :didattica:magistrale:svl:ay_1819:svl-notes-03-06-2019.pdf |Notes}} ---- ===== 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_1819:1_-_introduction_to_model_checking.pdf | Introduction to Model Checking}} * {{ :didattica:magistrale:svl:ay_1819:2_-_transition_systems.pdf |Transition Systems}} * {{ :didattica:magistrale:svl:ay_1819:3_-_modelling_hardware_circuits.pdf |Modelling Hardware Circuits}} * {{ :didattica:magistrale:svl:ay_1819:4_-_program._graphs.pdf |Program Graphs}} * {{ :didattica:magistrale:svl:ay_1819: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_1819:6_-_parallelism._interleaving_for_ts.pdf |Parallelism: Interleaving for Transition Systems}} * {{ :didattica:magistrale:svl:ay_1819:7_-_parallelism._interleaving_for_program_graphs.pdf |Parallelism: Interleaving for Program Graphs}} * {{ :didattica:magistrale:svl:ay_1819:8_-_parallelism_and_communication._synchronous_message_passing.pdf |Parallelism and Communication: Synchronous Message Passing}} * {{ :didattica:magistrale:svl:ay_1819:9_-_parallelism_and_communication._channel_systems.pdf |Parallelism and Communication: Channel Systems}} * {{ :didattica:magistrale:svl:ay_1819:10_-_parallelism_and_communication._synchronous_product.pdf |Parallelism and Communication: Synchronous Product}} * {{ :didattica:magistrale:svl:ay_1819:11_-_nanopromela_semantics.pdf |Structural Operational Semantics of NanoPROMELA}} **Linear Time Properties** * {{ :didattica:magistrale:svl:ay_1819:1_-_linear_time_properties._introduction.pdf |Introduction to Linear Time Properties}} * {{ :didattica:magistrale:svl:ay_1819:2_-_linear_time_properties._definition_and_satisfaction._trace_equivalence.pdf |Definition and Satisfaction, Trace Equivalence}} * {{ :didattica:magistrale:svl:ay_1819:3_-_linear_time_properties._invariants_and_invariant_checking.pdf |Invariants and Invariant Checking}} * {{ :didattica:magistrale:svl:ay_1819:4_-_linear_time_properties._safety_properties._bad_prefixes_and_prefix_closure.pdf |Safety Properties}} * {{ :didattica:magistrale:svl:ay_1819:5_-_linear_time_properties._liveness_properties.pdf |Liveness Properties}} * {{ :didattica:magistrale:svl:ay_1819:6_-_linear_time_properties._decomposition_theorem.pdf |Decomposition Theorem}} * {{ :didattica:magistrale:svl:ay_1819:7_-_linear_time_properties._fairness.pdf |Fairness}} **Linear Time Logic (LTL)** * {{ :didattica:magistrale:svl:ay_1819:1_-_ltl_syntax_and_semantics.pdf |Syntax and Semantics of LTL}} * {{ :didattica:magistrale:svl:ay_1819:2_-_ltl_equivalences_and_laws.pdf |Equivalences and Laws of LTL}} * {{ :didattica:magistrale:svl:ay_1819:3_-_ltl_expressing_fairness.pdf |Expressing Fairness in LTL}} **Computation Tree Logic (CTL)** * {{ :didattica:magistrale:svl:ay_1819:1_-_ctl_syntax_semantics_equivalences_and_normal_forms.pdf |Syntax, Semantics, Equivalences and Normal Forms of CTL}} * {{ :didattica:magistrale:svl:ay_1819:2_-_ctl_vs_ltl.pdf |CTL versus LTL}} * {{ :didattica:magistrale:svl:ay_1819:4_-_ctl_with_fairness.pdf |CTL with Fairness}} ==== Timed Systems ==== **Timed Automata** * {{ :didattica:magistrale:svl:ay_1819:1_-_timed_automata.pdf |Timed Automata}} * {{ :didattica:magistrale:svl:ay_1819:2_-_timed_paths_divergence_timelocks_zenoness.pdf |Timed Paths, Divergence, Timelocks, Zenoness}} * {{ :didattica:magistrale:svl:ay_1819: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_1819:exsolmodelsandmodelling.pdf |Transition Systems and Modelling Languages for Reactive Systems}} * {{ :didattica:magistrale:svl:ay_1819:exsollineartime.pdf |Linear Time Properties}} * {{ :didattica:magistrale:svl:ay_1819: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. ==== 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 ===== - {{ :didattica:magistrale:svl:ay_1819:svl18q9_project.pdf |Text of Project 2018/2019}} ---- ===== Exams ===== **Exam Dates A.Y. 2018/2019 (Written Test Dates)** - 06/02/2019, 3:00pm, Room LA1 - no students. - 20/02/2019, 3:00pm, Room LA1 - no students. - 13/06/2019, 3:00pm, Room AB1 - no students. - 27/06/2019, 3:00pm, Room TBA, 28/06/2019, 11:00am, Room AB1 Polo Lodovici - {{ :didattica:magistrale:svl:ay_1819:svl1819appello1.pdf |Text}}, {{ :didattica:magistrale:svl:ay_1819:svl1819appello1solutionwithnotes.pdf |Text with Solutions}} - 17/07/2019, 3:00pm, Room AB2 Polo Lodovici - {{ :didattica:magistrale:svl:ay_1819:svl1819appello2.pdf |Text}}, {{ :didattica:magistrale:svl:ay_1819:svl1819appello2withsolution.pdf |Text with Solutions}} - 12/09/2019, 3:00pm, Room AA1 Polo Lodovici - {{ :didattica:magistrale:svl:ay_1819:svl1819appello3.pdf |Text}}, {{ :didattica:magistrale:svl:ay_1819:svl1819appello3_with_solutions.pdf |Text with Solutions}} - 26/09/2019, 3:00pm, Room AA1 Polo Lodovici, please register on ESSE3 to the Partial Exam "SVL1819 Sess. VII - Written Test" before 20/09/2019 - 24/03/2020, 3:00pm, Room TBA, please register on ESSE3 to the Partial Exam "SVL1819 Sess. VIII - Written Test" before 20/03/2020 **Exam rules** The exam consists of a written test, containing open-answer questions (exercises), together with one project, realised with the tools introduced in the course (see section "Project" 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. BSc students or MSc students who did not select the Intelligent and Adaptive Systems (IAS) Curriculum will not be able to register for the written test until they communicate to the Secretary Office (Tiziana Jajani c/o Student Secretary Office, [[http://www.unicam.it/studente/segreterie-studenti|Opening Hours]]) their choice to attend to this course, code [ST1192] SYSTEMS VERIFICATION LAB. 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 SVL1819-Project-APP-X-Surname-Name where 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 francesco.tiezzi@unicam.it by 11.59pm of the day specified for the Partial Exam "SVL1819 Sess. X - Project Deliver" relative to Session X. **Students should also register for this Partial Exam within the day before on ESSE3**. ** 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. ----