Differences

This shows you the differences between two versions of the page.

--- didattica:magistrale:svl:ay_2021:main [2020/09/29 13:55]
luca
+++ didattica:magistrale:svl:ay_2021:main [2021/06/10 10:26] (current)
luca [Exams]
@@ Line 20: / Line 20: @@
 **Lectures schedule**:
-  * TBD Second Semester
+  * From March 3rd 2021 - Wednesdays from 2.00pm to 4.00pm - Fridays from 11.00am to 1.00pm
 **Recording of Lectures and other material**:
-  * TBD
+  * The recordings and other material will be given on the **Google Classroom** platform: [[https://classroom.google.com/c/MjkxNDU4MTYwNjA5?cjc=557nyk5]] (login with @studenti.unicam.it credentials)
 **Webex Room for Lecture Streaming**
@@ Line 52: / Line 52: @@
 ===== Lectures =====
-  * TBD
+  * The recordings and other material will be given on the **Google Classroom** platform: [[https://classroom.google.com/c/MjkxNDU4MTYwNjA5?cjc=557nyk5]] (login with @studenti.unicam.it credentials)
 ----
@@ Line 60: / Line 60: @@
 ==== Verification Tools ====
   * [[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]]
@@ Line 77: / Line 78: @@
   * [[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]]
 ==== Reactive Systems ====
 **Transition Systems and Modelling Languages for Reactive Systems**
-  * {{ :didattica:magistrale:svl:ay_2021:1_-_introduction_to_model_checking.pdf | Introduction to Model Checking}}
+  * {{ :didattica:magistrale:svl:ay_1920:1_-_introduction_to_model_checking.pdf | Introduction to Model Checking}}
-  * {{ :didattica:magistrale:svl:ay_2021:2_-_transition_systems.pdf |Transition Systems}}
+  * {{ :didattica:magistrale:svl:ay_1920:2_-_transition_systems.pdf |Transition Systems}}
-  * {{ :didattica:magistrale:svl:ay_2021:3_-_modelling_hardware_circuits.pdf |Modelling Hardware Circuits}}
+  * {{ :didattica:magistrale:svl:ay_1920:3_-_modelling_hardware_circuits.pdf |Modelling Hardware Circuits}}
-  * {{ :didattica:magistrale:svl:ay_2021:4_-_program._graphs.pdf |Program Graphs}}
+  * {{ :didattica:magistrale:svl:ay_1920:4_-_program._graphs.pdf |Program Graphs}}
-  * {{ :didattica:magistrale:svl:ay_2021: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: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_2021:6_-_parallelism._interleaving_for_ts.pdf |Parallelism: Interleaving for Transition Systems}}
+  * {{ :didattica:magistrale:svl:ay_1920:6_-_parallelism._interleaving_for_ts.pdf |Parallelism: Interleaving for Transition Systems}}
-  * {{ :didattica:magistrale:svl:ay_2021:7_-_parallelism._interleaving_for_program_graphs.pdf |Parallelism: Interleaving for Program Graphs}}
+  * {{ :didattica:magistrale:svl:ay_1920:7_-_parallelism._interleaving_for_program_graphs.pdf |Parallelism: Interleaving for Program Graphs}}
-  * {{ :didattica:magistrale:svl:ay_2021:8_-_parallelism_and_communication._synchronous_message_passing.pdf |Parallelism and Communication: Synchronous Message Passing}}
+  * {{ :didattica:magistrale:svl:ay_1920:8_-_parallelism_and_communication._synchronous_message_passing.pdf |Parallelism and Communication: Synchronous Message Passing}}
-  * {{ :didattica:magistrale:svl:ay_2021:9_-_parallelism_and_communication._channel_systems.pdf |Parallelism and Communication: Channel Systems}}
+  * {{ :didattica:magistrale:svl:ay_1920:9_-_parallelism_and_communication._channel_systems.pdf |Parallelism and Communication: Channel Systems}}
-  * {{ :didattica:magistrale:svl:ay_2021:10_-_parallelism_and_communication._synchronous_product.pdf |Parallelism and Communication: Synchronous Product}}
+  * {{ :didattica:magistrale:svl:ay_1920:10_-_parallelism_and_communication._synchronous_product.pdf |Parallelism and Communication: Synchronous Product}}
-  * {{ :didattica:magistrale:svl:ay_2021:11_-_nanopromela_semantics.pdf |Structural Operational Semantics of NanoPROMELA}}
+  * {{ :didattica:magistrale:svl:ay_1920:11_-_nanopromela_semantics.pdf |Structural Operational Semantics of NanoPROMELA}}
 **Linear Time Properties**
-  * {{ :didattica:magistrale:svl:ay_2021:1_-_linear_time_properties._introduction.pdf |Introduction to Linear Time Properties}}
+  * {{ :didattica:magistrale:svl:ay_1920:1_-_linear_time_properties._introduction.pdf |Introduction to Linear Time Properties}}
-  * {{ :didattica:magistrale:svl:ay_2021:2_-_linear_time_properties._definition_and_satisfaction._trace_equivalence.pdf |Definition and Satisfaction, Trace Equivalence}}
+  * {{ :didattica:magistrale:svl:ay_1920:2_-_linear_time_properties._definition_and_satisfaction._trace_equivalence.pdf |Definition and Satisfaction, Trace Equivalence}}
-  * {{ :didattica:magistrale:svl:ay_2021:3_-_linear_time_properties._invariants_and_invariant_checking.pdf |Invariants and Invariant Checking}}
+  * {{ :didattica:magistrale:svl:ay_1920:3_-_linear_time_properties._invariants_and_invariant_checking.pdf |Invariants and Invariant Checking}}
-  * {{ :didattica:magistrale:svl:ay_2021:4_-_linear_time_properties._safety_properties._bad_prefixes_and_prefix_closure.pdf |Safety Properties}}
+  * {{ :didattica:magistrale:svl:ay_1920:4_-_linear_time_properties._safety_properties._bad_prefixes_and_prefix_closure.pdf |Safety Properties}}
-  * {{ :didattica:magistrale:svl:ay_2021:5_-_linear_time_properties._liveness_properties.pdf |Liveness Properties}}
+  * {{ :didattica:magistrale:svl:ay_1920:5_-_linear_time_properties._liveness_properties.pdf |Liveness Properties}}
-  * {{ :didattica:magistrale:svl:ay_2021:6_-_linear_time_properties._decomposition_theorem.pdf |Decomposition Theorem}}
+  * {{ :didattica:magistrale:svl:ay_1920:6_-_linear_time_properties._decomposition_theorem.pdf |Decomposition Theorem}}
-  * {{ :didattica:magistrale:svl:ay_2021:linear_time_properties._regular_safety_properties.pdf |Regular Safety Properties}}
+  * {{ :didattica:magistrale:svl:ay_1920:linear_time_properties._regular_safety_properties.pdf |Regular Safety Properties}}
-  * {{ :didattica:magistrale:svl:ay_2021:7_-_linear_time_properties._fairness.pdf |Fairness}}
+  * {{ :didattica:magistrale:svl:ay_1920:7_-_linear_time_properties._fairness.pdf |Fairness}}
 **Linear Time Logic (LTL)**
-  * {{ :didattica:magistrale:svl:ay_2021:1_-_ltl_syntax_and_semantics.pdf |Syntax and Semantics of LTL}}
+  * {{ :didattica:magistrale:svl:ay_1920:1_-_ltl_syntax_and_semantics.pdf |Syntax and Semantics of LTL}}
-  * {{ :didattica:magistrale:svl:ay_2021:2_-_ltl_equivalences_and_laws.pdf |Equivalences and Laws of LTL}}
+  * {{ :didattica:magistrale:svl:ay_1920:2_-_ltl_equivalences_and_laws.pdf |Equivalences and Laws of LTL}}
-  * {{ :didattica:magistrale:svl:ay_2021:3_-_ltl_expressing_fairness.pdf |Expressing Fairness in LTL}}
+  * {{ :didattica:magistrale:svl:ay_1920:3_-_ltl_expressing_fairness.pdf |Expressing Fairness in LTL}}
+  * {{ :didattica:magistrale:svl:ay_2021:4-5_soft_-_ltl_general_picture_of_automata-based_model_checking.pdf | General picture of LTL model checking}}
 **Computation Tree Logic (CTL)**
-  * {{ :didattica:magistrale:svl:ay_2021:1_-_ctl_syntax_semantics_equivalences_and_normal_forms.pdf |Syntax, Semantics, Equivalences and Normal Forms of 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_2021:2_-_ctl_vs_ltl.pdf |CTL versus LTL}}
+  * {{ :didattica:magistrale:svl:ay_2021:3_-_ctl_model_checking.pdf | Model Checking of CTL}}
-  * {{ :didattica:magistrale:svl:ay_2021:4_-_ctl_with_fairness.pdf |CTL with Fairness}}
+  * {{ :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_2021:1_-_timed_automata.pdf |Timed Automata}}
+  * {{ :didattica:magistrale:svl:ay_1920:1_-_timed_automata.pdf |Timed Automata}}
-  * {{ :didattica:magistrale:svl:ay_2021:2_-_timed_paths_divergence_timelocks_zenoness.pdf |Timed Paths, Divergence, Timelocks, Zenoness}}
+  * {{ :didattica:magistrale:svl:ay_1920:2_-_timed_paths_divergence_timelocks_zenoness.pdf |Timed Paths, Divergence, Timelocks, Zenoness}}
-  * {{ :didattica:magistrale:svl:ay_2021:3_-_timed_ctl.pdf |Timed CTL}}
+  * {{ :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]]
 ==== Exercises ====
 **Exercises with (some) solutions**
-  * {{ :didattica:magistrale:svl:ay_2021:exsolmodelsandmodelling.pdf |Transition Systems and Modelling Languages for Reactive Systems}}
+  * {{ :didattica:magistrale:svl:ay_1920:exsolmodelsandmodelling.pdf |Transition Systems and Modelling Languages for Reactive Systems}}
-  * {{ :didattica:magistrale:svl:ay_2021:exsollineartime.pdf |Linear Time Properties}}
+  * {{ :didattica:magistrale:svl:ay_1920:exsollineartime.pdf |Linear Time Properties}}
-  * {{ :didattica:magistrale:svl:ay_2021: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.
+  * {{ :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_2021:svl1819appello1.pdf |Text1}}, {{ :didattica:magistrale:svl:ay_2021:svl1819appello1solutionwithnotes.pdf |Text1 with Solutions}}
+  * {{ :didattica:magistrale:svl:ay_1920:svl1819appello1.pdf |Text1}}, {{ :didattica:magistrale:svl:ay_1920:svl1819appello1solutionwithnotes.pdf |Text1 with Solutions}}
-  * {{ :didattica:magistrale:svl:ay_2021:svl1819appello2.pdf |Text2}}, {{ :didattica:magistrale:svl:ay_2021:svl1819appello2withsolution.pdf |Text2 with Solutions}}
+  * {{ :didattica:magistrale:svl:ay_1920:svl1819appello2.pdf |Text2}}, {{ :didattica:magistrale:svl:ay_1920:svl1819appello2withsolution.pdf |Text2 with Solutions}}
-  * {{ :didattica:magistrale:svl:ay_2021:svl1819appello3.pdf |Text3}}, {{ :didattica:magistrale:svl:ay_2021:svl1819appello3_with_solutions.pdf |Text3 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**
@@ Line 150: / Line 152: @@
 ===== Project =====
 <WRAP box round center 95%>
-  - TBD
+  * 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)
 </WRAP>
@@ Line 164: / Line 166: @@
 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.
+**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**