Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
didattica:magistrale:rsv:ay_1718:main [2017/12/12 18:38] luca [Course Contents] |
didattica:magistrale:rsv:ay_1718:main [2020/09/17 16:55] (current) |
||
---|---|---|---|
Line 103: | Line 103: | ||
- Wed 06/12/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=5f3cdd0e6460f085dd76540b596903c2|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=1ca5f02bfb0f8d6de50698e7ba4de98f|Download Lecture]] | - Wed 06/12/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=5f3cdd0e6460f085dd76540b596903c2|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=1ca5f02bfb0f8d6de50698e7ba4de98f|Download Lecture]] | ||
- Thu 07/12/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=53409c42226f30dda49b8fb178a1b10e|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=097dd5f4c4e1fd2e9c4ba60440c95e7a|Download Lecture]], {{ :didattica:magistrale:rsv:ay_1718:rsv1718-07-12-2017.pdf |Notes}} | - Thu 07/12/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=53409c42226f30dda49b8fb178a1b10e|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=097dd5f4c4e1fd2e9c4ba60440c95e7a|Download Lecture]], {{ :didattica:magistrale:rsv:ay_1718:rsv1718-07-12-2017.pdf |Notes}} | ||
+ | - Wed 13/12/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=920643cd497e4c61097e764f485f929b|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=0068e7e1909f545858083069e3a6fd93|Download Lecture]], {{ :didattica:magistrale:rsv:ay_1718:archivio_2.zip |Promela examples}} | ||
+ | - Thu 14/12/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=873cf911a8174260930a60e45f1a154f|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=addb93a338db11efd7bdc109cf3cb7eb|Download Lecture]], {{ :didattica:magistrale:rsv:ay_1718:rsv1718-14-12-17.pdf |Notes}} | ||
+ | - Wed 20/12/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=0f6946a123e88f99cb782d112a23312e|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=f8b2a081bef0ece513713af61729a645|Download Lecture]] | ||
+ | - Thu 21/12/2017 [[https://unicam.webex.com/unicam/ldr.php?RCID=cd23d6aada95af82585445c28e7b3fc5|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=a71119e9c0a53491e873a8d892a2ad8d|Download Lecture]] | ||
+ | - Wed 10/01/2018 [[https://unicam.webex.com/unicam/ldr.php?RCID=459f21a454d016c0dda6ec64eba09f16|Watch Lecture]], [[https://unicam.webex.com/unicam/lsr.php?RCID=87a4afabf4853ece2eb978f06e652648|Download Lecture]], {{ :didattica:magistrale:rsv:ay_1718:rsv1718-10-01-2018.pdf |Notes}} | ||
+ | - Thu 11/01/2018 [[https://unicam.webex.com/unicam/ldr.php?RCID=f6e41fedc34f62111a6de0446d91aec7|Watch Lecture First Part]], [[https://unicam.webex.com/unicam/lsr.php?RCID=4c07b2c130a4ceb5c808bb717683df27|Download Lecture First Part]], [[https://unicam.webex.com/unicam/ldr.php?RCID=975bef9d11f823fda196f7d2551b997e|Watch Lecture Second Part]], [[https://unicam.webex.com/unicam/lsr.php?RCID=3bfce3dada4d222f0646253c0db408cf|Download Lecture Second Part]], {{ :didattica:magistrale:rsv:ay_1718:rsv1718-11-01-18.pdf |Notes}} | ||
</WRAP> | </WRAP> | ||
---- | ---- | ||
Line 154: | Line 160: | ||
//Linear Temporal Logic// | //Linear Temporal Logic// | ||
- | * {{ :didattica:magistrale:rsv:ay_1718:ltl._syntax_and_semantics.pdf |LTL Syntax and Semantics}} | + | * {{ :didattica:magistrale:rsv:ay_1718:1_-_ltl_syntax_and_semantics.pdf |LTL syntax and semantics}} - **Updated 13/12/17** |
- | * {{ :didattica:magistrale:rsv:ay_1718:ltl._expressing_fairness.pdf |Expressing Fairness in LTL}} | + | * {{ :didattica:magistrale:rsv:ay_1718:2_-_ltl_equivalences_and_laws.pdf |LTL equivalences and laws}} - **Updated 13/12/17** |
- | * {{ :didattica:magistrale:rsv:ay_1718:ltl._general_picture_of_model_checking_with_buchi_automata.pdf |General Picture of LTL Model Checking with Buchi Automata}} | + | * {{ :didattica:magistrale:rsv:ay_1718:3_-_ltl_expressing_fairness.pdf |Expressing fairness in LTL}} - **Updated 13/12/17** |
+ | * {{ :didattica:magistrale:rsv:ay_1718:4_-_ltl_general_picture_of_model_checking_with_buchi_automata.pdf |General Picture of LTL model checking with omega automata and complexity}} - **Updated 13/12/17** | ||
- | //Computational Tree Logic// | + | //Computation Tree Logic// |
* {{ :didattica:magistrale:rsv:ay_1718:ctl._syntax_semantics_equivalences_and_normal_forms.pdf |CTL: Syntax, Semantics, Equivalence and Normal Forms}} | * {{ :didattica:magistrale:rsv:ay_1718:ctl._syntax_semantics_equivalences_and_normal_forms.pdf |CTL: Syntax, Semantics, Equivalence and Normal Forms}} | ||
Line 202: | Line 209: | ||
<WRAP box round center 95%> | <WRAP box round center 95%> | ||
**Exam Dates A.Y. 2017/2018** | **Exam Dates A.Y. 2017/2018** | ||
- | - Appello I - Written Test on Thursday 01/02/2018 at 3.00pm, Room TBA | + | - Appello I - Written Test on Thursday 01/02/2018 at 3.00pm, Room AB3 Polo Lodovici - {{ :didattica:magistrale:rsv:ay_1718:rsv1718appello1.pdf |Written Test Text}}, {{ :didattica:magistrale:rsv:ay_1718:rsv1718app1sol.pdf |Written Test Solution}} |
- | - Appello II - Written Test on Thursday 15/02/2018 at 3.00pm, Room TBA | + | - Appello II - Written Test on Thursday 15/02/2018 at 3.00pm, Room AB3 Polo Lodovici - {{ :didattica:magistrale:rsv:ay_1718:rsv1718appello2.pdf |Written Test Text}}, {{ :didattica:magistrale:rsv:ay_1718:rsv1718app2sol.pdf |Written Test Solution}} |
- | - Appello III - Written Test on Wednesday 20/06/2018 at 3.00pm, Room TBA | + | - Appello III - Written Test on Wednesday 20/06/2018 at 3.00pm, Room AB3 Polo Lodovici - No Students |
- | - Appello IV - Written Test on Wednesday 11/07/2018 at 3.00pm, Room TBA | + | - Appello IV - Written Test on Wednesday 11/07/2018 at 10.00am, Room AB3 Polo Lodovici - {{ :didattica:magistrale:rsv:ay_1718:rsv1718appello4.pdf |Written Test Text}}, {{ :didattica:magistrale:rsv:ay_1718:rsv1718app4sol.pdf |Written Test Solution}} |
- | - Appello V - Written Test on Wednesday 12/09/2018 at 3.00pm, Room TBA | + | - Appello V - Written Test on Wednesday 12/09/2018 at 10.00am, Room AB3 Polo Lodovici |
- | - Appello VI - Written Test on Wednesday 26/09/2018 at 3.00pm, Room TBA | + | - Appello VI - Written Test on Wednesday 26/09/2018 at 3.00pm, Room AB3 Polo Lodovici |
- Appello VII - Written Test on Wednesday 06/02/2019 at 3.00pm, Room TBA | - Appello VII - Written Test on Wednesday 06/02/2019 at 3.00pm, Room TBA | ||
- Appello VIII - Written Test on Wednesday 20/02/2019 at 3.00pm, Room TBA | - Appello VIII - Written Test on Wednesday 20/02/2019 at 3.00pm, Room TBA | ||
Line 219: | Line 226: | ||
**Exam rules** | **Exam rules** | ||
- | The exam consists of a written test, containing open-answer and/or closed-answer questions, together with one project, realised with a model checking tool (see section "Projects" above). The project must be sent the day before the written test to which the student is registered (see section "Instructions for Sending Projects" below). During the exercise sessions throughout the course samples of the written test questions will be presented with solutions. During the written test will students can consult a hand-written A4 paper of their production for reference. | + | The exam consists of a written test, containing open-answer and/or closed-answer questions, together with one project, realised with a model checking tool (see section "Projects" above). The project must be sent the day before the written test to which the student is registered (see section "Instructions for Sending Projects" below). 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. BSc students or MSc students who did not select the Software Modelling and Verification (SMV) Curriculum will not be able to register for the written test until they communicate to the Secretary Office (Tiziana Jajani c/o Student Secretary Office at Campus, Via D'Accorso SNC, Camerino [[http://www.unicam.it/studente/segreterie-studenti|Opening Hours]]) their choice to attend to this course, code [ST1113] REACTIVE SYSTEMS VERIFICATION. | **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. BSc students or MSc students who did not select the Software Modelling and Verification (SMV) Curriculum will not be able to register for the written test until they communicate to the Secretary Office (Tiziana Jajani c/o Student Secretary Office at Campus, Via D'Accorso SNC, Camerino [[http://www.unicam.it/studente/segreterie-studenti|Opening Hours]]) their choice to attend to this course, code [ST1113] REACTIVE SYSTEMS VERIFICATION. | ||
- | Please note that any student who did not send the project the day before the written test **will be excluded** from the written test. In case of re-trying of the written test the project must be re-sent. | + | Please note that any student who did not send the project the day before the written test **may be excluded** from the written test. In case of re-trying of the written test the project must be re-sent. |
**Instructions for Sending Projects** | **Instructions for Sending Projects** |