Differences

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

--- didattica:ay2122:englishb2:main [2022/03/02 11:26] – [Exams] luca
+++ didattica:ay2122:englishb2:main [2022/03/02 12:23] – [Exams] luca
@@ Line 86: / Line 86: @@
     * [[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)
-==== 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>
@@ Line 162: / Line 102: @@
 **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**