Differences

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

--- didattica:magistrale:svl:ay_2021:main [2021/03/02 10:54]
luca [General Info]
+++ didattica:magistrale:svl:ay_2021:main [2021/06/10 10:26] (current)
luca [Exams]
@@ 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 ====
@@ Line 107: / Line 111: @@
   * {{ :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}}
@@ Line 160: / 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**