Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
didattica:magistrale:rtpsv:ay_1718:main [2017/09/20 13:44] luca [General Info] |
didattica:magistrale:rtpsv:ay_1718:main [2020/09/17 16:55] (current) |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Real-time and Probabilistic System Verification ====== | + | ====== Real-time and Probabilistic Systems Verification ====== |
| ---- | ---- | ||
| ===== News ===== | ===== News ===== | ||
| <WRAP center round important 95%> | <WRAP center round important 95%> | ||
| * <wrap em>**October 2nd, 2017**</wrap>: The course starts officially at 11.00 in Room LA1 | * <wrap em>**October 2nd, 2017**</wrap>: The course starts officially at 11.00 in Room LA1 | ||
| + | * <wrap em>**October 12th 2017**</wrap>: the lecture of Thursday 12th October is cancelled for a commitment of the teacher. | ||
| + | * <wrap em>**October 30th 2017**</wrap>: the lecture of Thursday 9th November is cancelled for a commitment of the teacher. | ||
| </WRAP> | </WRAP> | ||
| Line 83: | Line 85: | ||
| </WRAP> | </WRAP> | ||
| ---- | ---- | ||
| - | ===== Study material ===== | + | ===== Study Material ===== |
| <WRAP box round center 95%> | <WRAP box round center 95%> | ||
| - | **Lectures** | + | **Additional Material besides the Reference Books** |
| - | * Lecture of 03/10/2016 - {{ :didattica:magistrale:rtpsv:ay_1718:strong_bisimilarity.pdf |Strong Bisimilarity}}, {{ :didattica:magistrale:rtpsv:ay_1718:exercises_strong_bisimilarity_with_solutions.pdf |Exercises on Strong Bisimilarity}} - Reactive Systems Book pages: 31-53 | + | * {{ :didattica:magistrale:rtpsv:ay_1718:strong_bisimilarity.pdf |Strong Bisimilarity}}, {{ :didattica:magistrale:rtpsv:ay_1718: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_1718:weak_bisimilarity.pdf |Weak Bisimilarity}}, {{ :didattica:magistrale:rtpsv:ay_1718:weak_bisimilarity_exercises_with_solutions.pdf |Exercises on Weak Bisimilarity}}, {{ :didattica:magistrale:rtpsv:ay_1718:hennessy-milner_logic.pdf |Hennessy-Milner Logic (HML)}} - Reactive Systems Book pages: 53 - 72 and 89 - 101 | + | * {{ :didattica:magistrale:rtpsv:ay_1718:weak_bisimilarity.pdf |Weak Bisimilarity}}, {{ :didattica:magistrale:rtpsv:ay_1718:weak_bisimilarity_exercises_with_solutions.pdf |Exercises on Weak Bisimilarity}}, {{ :didattica:magistrale:rtpsv:ay_1718: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_1718:tarski_s_fixpoint_theorem.pdf | Tarski's Fixpoint Theorem}}, {{ :didattica:magistrale:rtpsv:ay_1718:bisimulation_as_a_fixed_point.pdf |Bisimulation as a fixed point}}, {{ :didattica:magistrale:rtpsv:ay_1718: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 | + | * {{ :didattica:magistrale:rtpsv:ay_1718:tarski_s_fixpoint_theorem.pdf | Tarski's Fixpoint Theorem}}, {{ :didattica:magistrale:rtpsv:ay_1718:bisimulation_as_a_fixed_point.pdf |Bisimulation as a fixed point}}, {{ :didattica:magistrale:rtpsv:ay_1718: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 |
| - | * <del>Lecture of 12/10/2016</del> - Lecture cancelled for Project Meeting | + | * {{ :didattica:magistrale:rtpsv:ay_1718: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_1718:ex_and_solutions_bisim_hml_weak_fixpoint.pdf |Exercise book}} posted for the last lecture |
| - | * Lecture of 17/10/2016 - {{ :didattica:magistrale:rtpsv:ay_1718: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_1718:ex_and_solutions_bisim_hml_weak_fixpoint.pdf |Exercise book}} posted for the last lecture | + | * {{ :didattica:magistrale:rtpsv:ay_1718:state-based_bisimilarity_and_bisimulation_quotient.pdf |State-based bisimilarity and Bisimulation quotient}} - Principles of MC Book pages: 449 - 468, {{ :didattica:magistrale:rtpsv:ay_1718:computing_bisimulation_quotient.pdf |Algorithms for computing the bisimulation quotient}} - Principles of MC Book pages: 476 - 493, {{ :didattica:magistrale:rtpsv:ay_1718:ctl_ctl-star_and_bisimulation_equivalence.pdf |CTL, CTL* and Bisimulation Equivalence}} - Principles of MC Book pages: 468 - 476 |
| - | * <del>Lecture of 19/10/2016</del> - Lectures suspended for Career Day | + | * 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 24/10/2016 - {{ :didattica:magistrale:rtpsv:ay_1718:state-based_bisimilarity_and_bisimulation_quotient.pdf |State-based bisimilarity and Bisimulation quotient}} - Principles of MC Book pages: 449 - 468, {{ :didattica:magistrale:rtpsv:ay_1718:computing_bisimulation_quotient.pdf |Algorithms for computing the bisimulation quotient}} - Principles of MC Book pages: 476 - 493, {{ :didattica:magistrale:rtpsv:ay_1718:ctl_ctl-star_and_bisimulation_equivalence.pdf |CTL, CTL* and Bisimulation Equivalence}} - Principles of MC Book pages: 468 - 476 | + | * 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_1718:exercises_on_tccs_with_some_solutions.pdf |Exercises on TCCS Modelling and Derivations}} |
| - | * 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. | + | * Timed Automata: Syntax and Semantics {{ :didattica:magistrale:rtpsv:ay_1718:ta_14-12-2016_tesei.pdf | Slides}} |
| - | * <del>Lecture of 31/10/2016</del> - Halloween vacation | + | * Syntax and semantics of Networks of Timed Automata (see previous Slides), [[http://www.uppaal.org|The UPPAAL Tool]], [[http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf|Tutorial on UPPAAL]] |
| - | * <del>Lecture of 02/11/2016</del> - Lecture suspended due to earthquake | + | * UPPAAL Exercises: JobShop, Fischer's Mutual Exclusion protocol, {{ :didattica:magistrale:rtpsv:ay_1718:uppaalexerciseslectures-21-12-16.zip |UPPAAL Code }}, [[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_1718:exercises_on_timed_automata_timed_bisimulation_region_graphs_with-_some_-solutions.pdf |Exercises on Timed Automata, Timed Bisimulation, Region Graphs}} |
| - | * <del>Lecture of 07/11/2016</del> - Lecture suspended due to earthquake | + | * 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_1718:uppaalexerciseslectures-22-12-16.zip |Exercises on UPPAAL}} |
| - | * <del>Lecture of 09/11/2016</del> - Lecture suspended due to earthquake | + | * Timed equivalences. {{ :didattica:magistrale:rtpsv:ay_1718:timed_equivalences.pdf |Slides 1}}, {{ :didattica:magistrale:rtpsv:ay_1718:luca.tesei_11-01-2017_11-24-58-slides.pdf |Slides 2}}. |
| - | * <del>Lecture of 14/11/2016</del> - Lecture suspended due to earthquake | + | * Regions and region graph, {{ :didattica:magistrale:rtpsv:ay_1718:region_graph.pdf |Slides 1}}, {{ :didattica:magistrale:rtpsv:ay_1718:luca_1.tesei_12-01-2017_11-52-47.pdf |Slides 2}}. |
| - | * <del>Lecture of 16/11/2016</del> - Lecture suspended due to earthquake | + | * Zones, forward reachability analysis with zones, time divergence, time locks, zeno paths. {{ :didattica:magistrale:rtpsv:ay_1718:luca.tesei_26-01-2017_19-33-48.pdf |Minutes}}, {{ :didattica:magistrale:rtpsv:ay_1718:reachability_analysis_with_zones.pdf |Slides Zones}} {{ :didattica:magistrale:rtpsv:ay_1718: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]] |
| - | * <del>Lecture of 21/11/2016</del> - Lecture suspended due to earthquake | + | * TCTL, Model Checking for TCTL {{ :didattica:magistrale:rtpsv:ay_1718:tctl.pdf |Slides TCTL Model Checking}} |
| - | * <del>Lecture of 23/11/2016</del> - Lecture suspended due to earthquake | + | * 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_1718:luca.tesei_01-02-2017_12-25-06.pdf |Notes}} |
| - | * <del>Lecture of 28/11/2016</del> - Lecture suspended due to earthquake | + | * 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_1718:luca.tesei_02-02-2017_11-16-02.pdf |Notes}} |
| - | * <del>Lecture of 30/11/2016</del> - Lecture suspended due to earthquake | + | * Exponential Distributions. Continuous Time Markov Chains. Examples in PRISM. {{ :didattica:magistrale:rtpsv:ay_1718:negative_exponential_distributions._continuous_time_markov_chains.pdf |Slides}}, [[http://www.prismmodelchecker.org/tutorial/power.php | PRISM Tutorial and example]] |
| - | * 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_1718:exercises_on_tccs_with_some_solutions.pdf |Exercises on TCCS Modelling and Derivations}} | + | * Continuous Stochastic Logic. Reachability Probabilities in MDPs. {{ :didattica:magistrale:rtpsv:ay_1718:continuous_stochastic_logic.pdf |Slides CSL}}, {{ :didattica:magistrale:rtpsv:ay_1718:reachability_probabilities_in_mdps.pdf |Slides MDPs}}, [[http://www.prismmodelchecker.org/tutorial/phil.php|Example of MDP in PRISM]] |
| - | * Lecture of 14/12/2016 - Timed Automata: Syntax and Semantics {{ :didattica:magistrale:rtpsv:ay_1718: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]] | + | * 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_1718:randomized_philosophers.pdf |Module relabelling for 3 and 5 philosophers}}, {{ :didattica:magistrale:rtpsv:ay_1718: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]] |
| - | * 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]] | + | * [[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_1718:simplified_ipv4_zeroconf_protocol_as_pta.pdf |Simplified protocol as PTA}}. [[http://www.prismmodelchecker.org/casestudies/molecules.php |Biochemical Reactions as CTMC]]. |
| - | * Lecture of 21/12/2016 - UPPAAL Exercises: JobShop, Fischer's Mutual Exclusion protocol, {{ :didattica:magistrale:rtpsv:ay_1718: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_1718: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_1718: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_1718:timed_equivalences.pdf |Slides 1}}, {{ :didattica:magistrale:rtpsv:ay_1718: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_1718:region_graph.pdf |Slides 1}}, {{ :didattica:magistrale:rtpsv:ay_1718: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 | + | |
| - | * <del>Lecture of 18/01/2017</del> - Lecture cancelled for bad weather conditions | + | |
| - | * <del>Lecture of 19/01/2017</del> - 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_1718:luca.tesei_26-01-2017_19-33-48.pdf |Minutes of the lecture}}, {{ :didattica:magistrale:rtpsv:ay_1718:reachability_analysis_with_zones.pdf |Slides Zones}} {{ :didattica:magistrale:rtpsv:ay_1718: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_1718: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_1718: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_1718: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_1718: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_1718:continuous_stochastic_logic.pdf |Slides CSL}}, {{ :didattica:magistrale:rtpsv:ay_1718: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_1718:randomized_philosophers.pdf |Module relabelling for 3 and 5 philosophers}}, {{ :didattica:magistrale:rtpsv:ay_1718: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_1718: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** | + | **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]] | * 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 | * Christel Baier, Joost-Pieter Katoen, “Principles of Model Checking”, The MIT Press, ISBN: 9780262026499 | ||
| + | |||
| + | **Reading Books** | ||
| + | * Vidyadhar G. Kulkarni, "Modeling and Analysis of Stochastic Systems, Third Edition", Chapman & Hall/CRC, 2016, ISBN-13: 978-1498756617 | ||
| * Michael Huth, Mark Ryan, “Logic in Computer Science: Modelling and Reasoning about Systems”, Cambridge University Press. ISBN: 9780521543101. | * 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. | * Glynn Winskel, "Formal Semantics of Programming Languages", The MIT Press, ISBN: 9780262731034. | ||
| </WRAP> | </WRAP> | ||
| ---- | ---- | ||
| + | ===== Projects ===== | ||
| + | <WRAP box round center 95%> | ||
| + | **Project(s) to be sent the day before the written test:** | ||
| + | - {{ :didattica:magistrale:rtpsv:ay_1718:rpsv1718_project.pdf |Project 2017-18}} | ||
| + | |||
| + | </WRAP> | ||
| + | |||
| + | ---- | ||
| + | |||
| ===== Exams ===== | ===== Exams ===== | ||
| <WRAP box round center 95%> | <WRAP box round center 95%> | ||
| - | **Assignments** | + | **Exam Dates A.Y. 2017/2018** |
| - | * 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 | + | - Appello I - Written Test on Tuesday 30/01/2018 at 3.00pm, Room TBA |
| - | * Assignment 2 - {{ :didattica:magistrale:rtpsv:ay_1718:rtpsv1617-assignment-2.pdf |Text of the Assignment}}, deadline 10/02/2017 23.59. | + | - Appello II - Written Test on Tuesday 13/02/2018 at 3.00pm, Room TBA |
| - | * Assignment 3 - {{ :didattica:magistrale:rtpsv:ay_1718:rpsv1617-assignment-3.pdf |Text of the Assignment}}, deadline 10/03/2017 23.59. | + | - Appello III - Written Test on Tuesday 19/06/2018 at 3.00pm, Room TBA |
| + | - Appello IV - Written Test on Tuesday 10/07/2018 at 3.00pm, Room TBA | ||
| + | - Appello V - Written Test on Tuesday 11/09/2018 at 3.00pm, Room TBA | ||
| + | - Appello VI - Written Test on Tuesday 25/09/2018 at 3.00pm, Room TBA | ||
| + | - Appello VII - Written Test on Tuesday 05/02/2019 at 3.00pm, Room TBA | ||
| + | - Appello VIII - Written Test on Wednesday 20/02/2019 at 11.00am, Room TBA | ||
| + | |||
| + | **Exam rules** | ||
| + | |||
| + | The exam consists of a written test, containing open-answer and/or closed-answer questions, together with one project, realised with a model checking tool (see section "Projects" above). The project must be sent the day before the written test to which the student is registered (see section "Instructions for Sending Projects" below). 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. | ||
| + | |||
| + | **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. | ||
| + | |||
| + | Please note that any student who did not send the project the day before the written test **may be excluded** from the written test. In case of re-trying of the written test the project must be re-sent. | ||
| + | |||
| + | **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 | ||
| + | |||
| + | RPSV1718-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 francesco.tiezzi@unicam.it by 11.59pm of the day before the written test scheduled for the selected session X. | ||
| - | **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 ** | ** Exam Results ** | ||
| - | * TBA | + | * 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. In case of acceptance, the grade will be registered in ESSE3. | ||
| </WRAP> | </WRAP> | ||
| + | ---- | ||
