====== Real-time and Probabilistic System Verification ====== ---- ===== News ===== * **September 7th, 2016**: the course web site is now on-line * **October 3rd, 2016**: first lecture * **November 2nd, 2016**: lectures are suspended form 27th October 2016 until further notice due to the earthquakes of the last days. ---- ===== General Info ===== **Teacher**: * [[http://docenti.unicam.it/pdett.aspx?ids=N&tv=d&UteId=572&ru=RU|Luca Tesei]] **Lessons schedule**: * Mon 5.00 am - 7.00 pm @ Room D. M. Ritchie, 2nd floor, Palazzo di Informatica (ex Tribunale), Piazza Mazzini 1, Camerino new time table and new room will be communicated as soon as information about the restart of lectures will be available * Wed 11.00 am - 1.00 pm @ Room D. M. Ritchie, 2nd floor, Palazzo di Informatica (ex Tribunale), Piazza Mazzini 1, Camerino new time table and new room will be communicated as soon as information about the restart of lectures will be available Lectures start on 3rd October 2016. New schedule after earthquake (from Wed 7/12/2016 on): * Wed 9.00 am - 11.00 am @ Room AB2, 2nd floor, Polo Lodovici, via Madonna delle Carceri 9, Camerino. * Thu 9.00 am - 11.00 am @ Room AB1, 2nd floor, Polo Lodovici, via Madonna delle Carceri 9, Camerino. **Students Office hours**: * Wed 3.00 pm - 5.00 pm - Luca Tesei's Room CS07 2nd Floor of Polo Tecnologico Palazzo Battibocca, via del Bastione 1, Camerino. Possible changes are advertised [[http://docenti.unicam.it/pdett.aspx?ids=N&tv=d&UteId=572&ru=RU|here]] * I will be available for online or face to face office hours by appointment, write to me at [[mailto:luca.tesei@unicam.it|luca.tesei@unicam.it]] **Prerequisites** * Having passed the course "Reactive Systems Verification" //alias// "Model Checking I" ---- ===== Course Objectives ===== **D1 – KNOWLEDGE AND UNDERSTANDING** At the end of the course, the student should be able to: - Understand the concept of bisimilarity and the algorithms for calculating a bisimulation - Understand the concept of action-based branching time logic - 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 clock regions and zones and illustrate how they can be used to realize the model checking of 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) **D2 – APPLYING KNOWLEDGE AND UNDERSTANDING** At the end of the course, the student should be able to: - Determine if two states of a transition system are bisimilar - Use the Hennessy-Milner Logic with recursion for specifying untimed properties - Use the formalism of Timed Automata to model real-time systems - Use the tool UPPAAL to verify real-time systems - Use the formalisms of DTMC, MDP and CTMC to model probabilistic or stochastic systems - Use the tool PRISM to verify probabilistic or stochastic systems **D3 – 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 **D4 - 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 **D5 – 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 timed, stochastic and probabilistic systems - Autonomously understand and learn to use new features added to tools for modelling and verifying timed, stochastic and probabilistic systems ---- ===== Course Contents ===== * Bisimilarity and bisimulation, calculating the quotient set through partition refinement. * Theory of fixed points. * Hennessy-Milner Logic with Recursion. * Real-time systems and timed formalisms. * Timed Automata. Timed Computation Tree Logic (TCTL). * Clock Regions and Zones. * 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. ---- ===== Study material ===== **Lectures** * Lecture of 03/10/2016 - {{ :didattica:magistrale:rtpsv:ay_1617:strong_bisimilarity.pdf |Strong Bisimilarity}}, {{ :didattica:magistrale:rtpsv:ay_1617:exercises_strong_bisimilarity_with_solutions.pdf |Exercises on Strong Bisimilarity}} - Reactive Systems Book pages: 31-53 * Lecture of 05/10/2016 - {{ :didattica:magistrale:rtpsv:ay_1617:weak_bisimilarity.pdf |Weak Bisimilarity}}, {{ :didattica:magistrale:rtpsv:ay_1617:weak_bisimilarity_exercises_with_solutions.pdf |Exercises on Weak Bisimilarity}}, {{ :didattica:magistrale:rtpsv:ay_1617:hennessy-milner_logic.pdf |Hennessy-Milner Logic (HML)}} - Reactive Systems Book pages: 53 - 72 and 89 - 101 * Lecture of 10/10/2016 - {{ :didattica:magistrale:rtpsv:ay_1617:tarski_s_fixpoint_theorem.pdf | Tarski's Fixpoint Theorem}}, {{ :didattica:magistrale:rtpsv:ay_1617:bisimulation_as_a_fixed_point.pdf |Bisimulation as a fixed point}}, {{ :didattica:magistrale:rtpsv:ay_1617:ex_and_solutions_bisim_hml_weak_fixpoint.pdf |Exercises and solution on Strong and Weak Bisimulation, HML and fixpoints}} Reactive Systems Book pages: 75 - 88 * Lecture of 12/10/2016 - Lecture cancelled for Project Meeting * Lecture of 17/10/2016 - {{ :didattica:magistrale:rtpsv:ay_1617:hennessy-milner_logic_with_recursively_defined_variables.pdf |HML with recursively defined variables}} - Reactive Systems Book pages: 105 - 120 - Exercises on HML, fixpoints and HML with recursion are in the {{ :didattica:magistrale:rtpsv:ay_1617:ex_and_solutions_bisim_hml_weak_fixpoint.pdf |Exercise book}} posted for the last lecture * Lecture of 19/10/2016 - Lectures suspended for Career Day * Lecture of 24/10/2016 - {{ :didattica:magistrale:rtpsv:ay_1617:state-based_bisimilarity_and_bisimulation_quotient.pdf |State-based bisimilarity and Bisimulation quotient}} - Principles of MC Book pages: 449 - 468, {{ :didattica:magistrale:rtpsv:ay_1617:computing_bisimulation_quotient.pdf |Algorithms for computing the bisimulation quotient}} - Principles of MC Book pages: 476 - 493, {{ :didattica:magistrale:rtpsv:ay_1617:ctl_ctl-star_and_bisimulation_equivalence.pdf |CTL, CTL* and Bisimulation Equivalence}} - Principles of MC Book pages: 468 - 476 * Lecture of 26/10/2016 - Timed Systems versus Untimed Systems: quantitative versus qualitative notion of time in models of software and hardware systems. Timed Labelled Transition Systems. Timed CCS: Syntax and Semantics. The principle of maximal process in Timed CCS (expressibility of time-outs). Examples. - Reactive Systems Book pages: 159 - 174. * Lecture of 31/10/2016 - Halloween vacation * Lecture of 02/11/2016 - Lecture suspended due to earthquake * Lecture of 07/11/2016 - Lecture suspended due to earthquake * Lecture of 09/11/2016 - Lecture suspended due to earthquake * Lecture of 14/11/2016 - Lecture suspended due to earthquake * Lecture of 16/11/2016 - Lecture suspended due to earthquake * Lecture of 21/11/2016 - Lecture suspended due to earthquake * Lecture of 23/11/2016 - Lecture suspended due to earthquake * Lecture of 28/11/2016 - Lecture suspended due to earthquake * Lecture of 30/11/2016 - Lecture suspended due to earthquake * Lecture of 07/12/2016 - Recall of TLTS and TCCS (Reactive Systems Book pages: 159 - 174). Definition of timed traces and timed languages (Reactive Systems Book pages: 193 - 195). Exercises on derivations of TCSS delay and action transitions. Exercises on existence of timed traces of TCCS processes. {{ :didattica:magistrale:rtpsv:ay_1617:exercises_on_tccs_with_some_solutions.pdf |Exercises on TCCS Modelling and Derivations}} * Lecture of 14/12/2016 - Timed Automata: Syntax and Semantics {{ :didattica:magistrale:rtpsv:ay_1617:ta_14-12-2016_tesei.pdf | "Slides" of the lecture with more slides and exercises for the lecture of 15/12/2016}} - [[https://cmr-em.webex.com/cmr-em-it/ldr.php?RCID=589992f9438a2cf086df5077bbb0fb03|Link to the online recording of the lecture]] * Lecture of 15/12/2016 - Syntax and semantics of Networks of Timed Automata (see Slides of 14/12/2016), [[http://www.uppaal.org|The UPPAAL Tool]], [[http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf|Tutorial on UPPAAL]], [[https://cmr-em.webex.com/cmr-em-it/ldr.php?RCID=69a54093b383f6b76115e9b2073bc687|Link to the online recording of the lecture]] * Lecture of 21/12/2016 - UPPAAL Exercises: JobShop, Fischer's Mutual Exclusion protocol, {{ :didattica:magistrale:rtpsv:ay_1617:uppaalexerciseslectures-21-12-16.zip |UPPAAL Code developed during lectures}}, [[https://www2.informatik.hu-berlin.de/~hs/Aktivitaeten/2011_Vino/Talks/Morning/11_Tom-Davies_Fischers-Algorithm.pdf|Slides on Fisher's Protocol]], [[https://books.google.it/books?id=PEXCnD7evqUC&pg=PA216&lpg=PA216&dq=fischer's+mutual+exclusion+protocol+starvation&source=bl&ots=k91dZqlCLU&sig=4x8I7Da5tKq9CiMC-_lzPLZKsK4&hl=it&sa=X&ved=0ahUKEwiM7cnmhITRAhUC1hoKHdemAb8Q6AEIKDAB#v=onepage&q=fischer's%20mutual%20exclusion%20protocol%20starvation&f=false|Discussion on starvation of Fischer's Protocol]] - {{ :didattica:magistrale:rtpsv:ay_1617:exercises_on_timed_automata_timed_bisimulation_region_graphs_with-_some_-solutions.pdf |Exercises on Timed Automata, Timed Bisimulation, Region Graphs}} - [[https://unicam.webex.com/unicam/ldr.php?RCID=06d7fe89e3c855e7b195490bd80d8bbf|Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=f89cd35c95d97d0fb9e22ff1353360cc|Link for downloading the lecture]] - Password to visualise and download the video: 78Fmpsg2 * Lecture of 22/12/2016 - Exercises on Timed Automata using UPPAAL: Fischer's mutual exclusion protocol, Gossipin Girls untimed and timed. Use of UPPAAL for determining the minimum number of calls to share all the secrets and the minimum amount of time to share all the secrets. Experiments on exponential state explosion. {{ :didattica:magistrale:rtpsv:ay_1617:uppaalexerciseslectures-22-12-16.zip |Exercises on UPPAAL developed during lecture}} - [[https://unicam.webex.com/unicam/ldr.php?RCID=4b92d5afacf5cb2ffb29a3be32cf2323|Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=ce2cc6037c947354dbabb713bd77d03f|Link for downloading the lecture]] - Password to visualise and download the video: TikwvMb2 * Lecture of 11/01/2017 - Timed equivalences. {{ :didattica:magistrale:rtpsv:ay_1617:timed_equivalences.pdf |Slides 1}}, {{ :didattica:magistrale:rtpsv:ay_1617:luca.tesei_11-01-2017_11-24-58-slides.pdf |Slides 2}}. [[https://unicam.webex.com/unicam/ldr.php?RCID=cd9c66ea4f12cba010ffa46c169e7eec|Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=a12e0bd24ee75d50e0da3eaf8a369be4 |Link for downloading the lecture]] - Password to visualise and download the video: uPEfPQ4c * Lecture of 12/01/2017 - Regions and region graph, {{ :didattica:magistrale:rtpsv:ay_1617:region_graph.pdf |Slides 1}}, {{ :didattica:magistrale:rtpsv:ay_1617:luca_1.tesei_12-01-2017_11-52-47.pdf |Slides 2}}. [[https://unicam.webex.com/unicam/ldr.php?RCID=2d5124197940c2d36f2d5c6e48e05fbf|Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=1009ec5b34484e0620efa1339ac2ee9a|Link for downloading the lecture]] - Password to visualise and download the video: 5Xvmp7dt * Lecture of 18/01/2017 - Lecture cancelled for bad weather conditions * Lecture of 19/01/2017 - Lecture cancelled for bad weather conditions * Lecture of 25/01/2017 - Zones, forward reachability analysis with zones, time divergence, time locks, zeno paths. {{ :didattica:magistrale:rtpsv:ay_1617:luca.tesei_26-01-2017_19-33-48.pdf |Minutes of the lecture}}, {{ :didattica:magistrale:rtpsv:ay_1617:reachability_analysis_with_zones.pdf |Slides Zones}} {{ :didattica:magistrale:rtpsv:ay_1617:time_divergence_timelocks_zenoness.pdf |Slides Time Divergence, Timelocks, Zenoness}}. [[https://unicam.webex.com/unicam/lsr.php?RCID=dcf7b1fede13492fbf68a28d3eb136b6 | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=830257830cf87fed39b24e4582bd0cb9|Link for downloading the lecture]] - Password to visualise and download the video: none * Lecture of 26/01/2017 - TCTL, Model Checking for TCTL {{ :didattica:magistrale:rtpsv:ay_1617:tctl.pdf |Slides TCTL Model Checking}} - [[https://unicam.webex.com/unicam/lsr.php?RCID=fd9b358f34ad49d698228c31c82fb09a | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=78261b24cead2af81b3b3396cbfbb852|Link for downloading the lecture]] - Password to visualise and download the video: none * Lecture of 01/02/2017 - Introduction to probabilistic systems and their verification. Definition of Discrete Time Markov Chain. Introduction to the tool PRISM. Examples of DTMC in PRISM. {{ :didattica:magistrale:rtpsv:ay_1617:luca.tesei_01-02-2017_12-25-06.pdf |Notes from the lecture}} - [[https://unicam.webex.com/unicam/ldr.php?RCID=405a578a3cfb5ded991a12f9d74b6ee4 | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=6e80b635f3cb266da01646f6b11369a5 |Link for downloading the lecture]] - Password to visualise and download the video: none * Lecture of 02/02/2017 - Definition of Cylinder Sets and of the probability measure on the set of paths of a DTMC. Formal syntax and semantics of PCTL. Introduction to Markov Decision Processes. {{ :didattica:magistrale:rtpsv:ay_1617:luca.tesei_02-02-2017_11-16-02.pdf |Notes form the lecture}} - [[https://unicam.webex.com/unicam/ldr.php?RCID=f23efe06edc31d6f1153d30e433e4629 | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=83d03c57dc60ffe0a9f8a12a38fca648 |Link for downloading the lecture]] - Password to visualise and download the video: none * Lecture of 08/02/2017 - Exponential Distributions. Continuous Time Markov Chains. Examples in PRISM. {{ :didattica:magistrale:rtpsv:ay_1617:negative_exponential_distributions._continuous_time_markov_chains.pdf |Slides}}, [[http://www.prismmodelchecker.org/tutorial/power.php | PRISM Tutorial and example]] - [[https://unicam.webex.com/unicam/ldr.php?RCID=75460821c878b5dee6cf4d1d742a3603 | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=3b9da98ee7f50dbe3165abd04e3ebb84 |Link for downloading the lecture]] - Password to visualise and download the video: none * Lecture of 09/02/2017 - Continuous Stochastic Logic. Reachability Probabilities in MDPs. {{ :didattica:magistrale:rtpsv:ay_1617:continuous_stochastic_logic.pdf |Slides CSL}}, {{ :didattica:magistrale:rtpsv:ay_1617:reachability_probabilities_in_mdps.pdf |Slides MDPs}}, [[http://www.prismmodelchecker.org/tutorial/phil.php|Example of MDP in PRISM]] - [[https://unicam.webex.com/unicam/ldr.php?RCID=849b4cf63dd75a91a309f64a404de0bf | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=a225cf7ef9f85508c971aeeb72da84fa |Link for downloading the lecture]] - Password to visualise and download the video: none * Lecture of 15/02/2017 - Exercises on Modelling and Verification of MDPs and CTMCs in PRISM. [[http://www.prismmodelchecker.org/tutorial/phil.php |Randomised Dining Philosophers]], {{ :didattica:magistrale:rtpsv:ay_1617:randomized_philosophers.pdf |Module relabelling for 3 and 5 philosophers}}, {{ :didattica:magistrale:rtpsv:ay_1617:lehman_d._rabin_m._o._1981_-_on_the_advantages_of_free_choice._a_symmetric_and_fully_distributed_solution_to_the_dining_philosophers_problem_extended_abstract_.pdf |Historical Paper on Randomised Dining Philosophers}}, and [[http://www.prismmodelchecker.org/tutorial/circadian.php |Circadian Clock]] - [[https://unicam.webex.com/unicam/ldr.php?RCID=8f0b6043f75073e47d038d549fc3aabc | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=125f269b776220e7dbab207bacac31ce |Link for downloading the lecture]] - Password to visualise and download the video: none * Lecture of 16/02/2017 - [[http://www.prismmodelchecker.org/manual/ThePRISMLanguage/PTAs |Probabilistic Timed Automata in PRISM]]. [[http://www.prismmodelchecker.org/casestudies/zeroconf.php |Simplified IPv4 ZeroConf Protocol]], {{ :didattica:magistrale:rtpsv:ay_1617:simplified_ipv4_zeroconf_protocol_as_pta.pdf |Simplified protocol as PTA}}. [[http://www.prismmodelchecker.org/casestudies/molecules.php |Biochemical Reactions as CTMC]]. - [[https://unicam.webex.com/unicam/ldr.php?RCID=0c65254ac79c72bd5e530c3538eaa829 | Link to the online recording of the lecture]] - [[https://unicam.webex.com/unicam/lsr.php?RCID=96b1ba89ded3cdc6586835882da0bb62 |Link for downloading the lecture]] - Password to visualise and download the video: none **Reference books** * Luca Aceto, Anna Ingolfsdottir, Kim Guldstrand Larsen and Jiri Srba, "Reactive Systems. Modelling, Specification and Verification", Cambridge University Press, 2007. ISBN: 9780521875462 – [[http://www.cambridge.org/us/knowledge/isbn/item1174475/?site_locale=en_US|Website]] * Christel Baier, Joost-Pieter Katoen, “Principles of Model Checking”, The MIT Press, ISBN: 9780262026499 * Michael Huth, Mark Ryan, “Logic in Computer Science: Modelling and Reasoning about Systems”, Cambridge University Press. ISBN: 9780521543101. * Glynn Winskel, "Formal Semantics of Programming Languages", The MIT Press, ISBN: 9780262731034. ---- ===== Exams ===== **Assignments** * Assignment 1 - Self-study report on "Partition-based minimization algorithm for Finite State Automata recognizing regular languages", deadline 14/10/2016 23.59. Send the pdf by email to luca.tesei@unicam.it * Assignment 2 - {{ :didattica:magistrale:rtpsv:ay_1617:rtpsv1617-assignment-2.pdf |Text of the Assignment}}, deadline 10/02/2017 23.59. * Assignment 3 - {{ :didattica:magistrale:rtpsv:ay_1617:rpsv1617-assignment-3.pdf |Text of the Assignment}}, deadline 10/03/2017 23.59. **Exam Dates A.Y. 2016/2017** * Winter session dates here * Summer session dates here * Autumn session dates here * Winter session dates here (2016) **Exam rules**: ** Exam Results ** * TBA