didattica:ay2122:englishb2:main

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision		 Previous revision
didattica:ay2122:englishb2:main [2022/03/02 11:26] – [Exams] lucadidattica:ay2122:englishb2:main [2022/03/09 17:26] (current) – luca
Line 56: Line 56:
 ==== Textbooks ==== ==== Textbooks ====
  
-  * Christel Baier, Joost-Pieter Katoen, “Principles of Model Checking”, The MIT Press, 2008.+  * Christel Baier, Joost-Pieter Katoen, "Principles of Model Checking", The MIT Press, 2008. 
 +  * Gerard J. Holzmann, "The SPIN model checker: Primer and Reference Manual", Addison-Wesley Professional, 2003.
  
 **Reference books** **Reference books**
Line 86: Line 87:
     * [[https://sourceforge.net/projects/redlib/|RED Model Checker]]     * [[https://sourceforge.net/projects/redlib/|RED Model Checker]]
  
-=== Slides, Codes and Exercises+==== Slides, Codes and Exercises ====
  
 All this material is accessible through the **Google Classroom** platform: [[https://classroom.google.com/c/NDU5OTY0NjM2MTE2?cjc=6meqjg2]] (login with @studenti.unicam.it credentials) All this material is accessible through the **Google Classroom** platform: [[https://classroom.google.com/c/NDU5OTY0NjM2MTE2?cjc=6meqjg2]] (login with @studenti.unicam.it credentials)
- 
-==== Reactive Systems ==== 
- 
-<del>**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}} 
-  * {{ :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_1920:1_-_ctl_syntax_semantics_equivalences_and_normal_forms.pdf |Syntax, Semantics, Equivalences and Normal Forms of CTL}} 
-  * {{ :didattica:magistrale:svl:ay_2021:3_-_ctl_model_checking.pdf | Model Checking 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]] 
- 
-==== 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}} 
-</del> 
- 
- 
  
 </WRAP> </WRAP>
Line 162: Line 103:
 **Exam Dates A.Y. 2021/2022**  **Exam Dates A.Y. 2021/2022** 
  
-Dates of Partial Exams "SVL2122 Sess. XXX - Project Delivery" and "SVL2021 Sess. XXX - Written Test" can be found in the [[https://didattica.unicam.it|ESSE3 Career System]] after login. +Dates of Partial Exams "SVL2122 Sess. XXX - Project Delivery" and "SVL2122 Sess. XXX - Written Test" can be found in the [[https://didattica.unicam.it|ESSE3 Career System]] after login. 
  
 **Exam rules** **Exam rules**
  • didattica/ay2122/englishb2/main.1646216776.txt.gz
  • Last modified: 2022/03/02 11:26
  • by luca