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/02/28 16:44] – [News] lucadidattica:ay2122:englishb2:main [2022/03/09 17:26] (current) – luca
Line 19: Line 19:
  
 **Recording of Lectures and other material**: **Recording of Lectures and other material**:
-  * The recordings and other material will be given on the **Google Classroom** platform: [[https://classroom.google.com/c/NDU5OTY0NjM2MTE2?cjc=6meqjg2]] (login with @studenti.unicam.it credentials)+  * The recordings of lectures and the material (slides, codes and exercises) will be given on the **Google Classroom** platform: [[https://classroom.google.com/c/NDU5OTY0NjM2MTE2?cjc=6meqjg2]] (login with @studenti.unicam.it credentials)
  
 **Webex Room for Lecture Streaming** **Webex Room for Lecture Streaming**
Line 54: Line 54:
 <WRAP box round center 95%> <WRAP box round center 95%>
  
-==== Verification Tools ====+==== Textbooks ==== 
 + 
 +  * 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** 
 +  * Michael Huth, Mark Ryan, "Logic in Computer Science", Second Edition, Cambridge University Press, 2004. ISBN: 9780521543101. 
 +  * Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba, "Reactive Systems", Cambridge University Press, 2007. 
 + 
 +==== Verification Tools Links ====
   * [[http://spinroot.com/spin/whatispin.html| SPIN Model Checker]]   * [[http://spinroot.com/spin/whatispin.html| SPIN Model Checker]]
     * [[https://spinroot.com/spin/Doc/SpinTutorial.pdf| Spin Tutorial]]     * [[https://spinroot.com/spin/Doc/SpinTutorial.pdf| Spin Tutorial]]
Line 78: Line 87:
     * [[https://sourceforge.net/projects/redlib/|RED Model Checker]]     * [[https://sourceforge.net/projects/redlib/|RED Model Checker]]
  
-==== Reactive Systems ====+==== Slides, Codes and Exercises ====
  
-**Transition Systems and Modelling Languages for Reactive Systems** +All this material is accessible through the **Google Classroom** platform: [[https://classroom.google.com/c/NDU5OTY0NjM2MTE2?cjc=6meqjg2]] (login with @studenti.unicam.it credentials)
-  * {{ :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}} +
-  *  +
- +
-==== Textbooks ==== +
- +
-  * Christel Baier, Joost-Pieter Katoen, “Principles of Model Checking”, The MIT Press, 2008. +
- +
-**Reference books** +
-  * Michael Huth, Mark Ryan, "Logic in Computer Science", Second Edition, Cambridge University Press, 2004. ISBN: 9780521543101. +
-  * Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen, Jiri Srba, "Reactive Systems", Cambridge University Press, 2007.+
  
 </WRAP> </WRAP>
Line 156: 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**
Line 166: Line 113:
 **Instructions for Sending Projects** **Instructions for Sending Projects**
  
-Students must create a folder in Google Drive, using the Google account associated to their email name.surname@studenti.unicam.it  +Instructions will be part of the Track of the project.
- +
-The folder must contain all the files relative to the project and a written report, in English, which describes all the phases of the developing of the project. The use of screenshots is encouraged to show, within the report, the runs and the results of the project.  +
- +
-The folder must be named  +
- +
-SVL2021-Project-N-APP-X-Surname-Name +
- +
-where N is the number of the realised project (according to the section "Projects" above) and X is the number of the exam session (Appello) as specified for each date of the written test above.  +
- +
-The folder must be shared (using Google Drive facilities) with luca.tesei@unicam.it and andrea.polini@unicam.it by 11.59pm of the day before the written test scheduled for the selected session X. +
- +
-Students that send the project must also register to the Partial Exam "SVL2021 Sess. XXX - Project Delivery" in ESSE3, specified for each exam session.  +
  
 ** Exam Results ** ** Exam Results **
  • didattica/ay2122/englishb2/main.1646063042.txt.gz
  • Last modified: 2022/02/28 16:44
  • by luca