Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
didattica:magistrale:svl:ay_2021:main [2021/04/21 16:09] luca [Material] |
didattica:magistrale:svl:ay_2021:main [2021/06/10 10:26] (current) luca [Exams] |
||
|---|---|---|---|
| Line 78: | Line 78: | ||
| * [[http://www.uppaal.org/| UPPAAL Model Checker]] | * [[http://www.uppaal.org/| UPPAAL Model Checker]] | ||
| * [[http://www.prismmodelchecker.org/| PRISM 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 ==== | ==== Reactive Systems ==== | ||
| Line 108: | Line 111: | ||
| * {{ :didattica:magistrale:svl:ay_1920: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_1920: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)** | **Computation Tree Logic (CTL)** | ||
| Line 162: | 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. | 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** | **Instructions for Sending Projects** | ||
