Formal Methods - Segédanyagok

Félév: 2020. tavasz
Title	Egyedi szöveg
Lecture 01: Course overview, introduction	EN_01a_Course_overview_2020.pdf EN_01b_role_of_formal_methods.pdf EN_01c_basic_formalisms.pdf
Lecture 02: Temporal logics, LTL	EN_02a_linear_temporal_logic.pdf
Lecture 03: Temporal logics, CTL, CTL*	EN_02b_branching_time_temporal_logics.pdf EN_02c_presented_models.zip
Lecture 04: Model checking	EN_03a_model_checking.pdf
Lecture 05: Efficient techniques for model checking	An online tool for building and visualizing ROBDDs: http://formal.cs.utah.edu:8080/pbl/BDD.php EN_04a_ROBDD_model checking.pdf EN_04b_bounded_model_checking.pdf
MIDTERM EXAM 1: Examples	EN_05b_practice_examples.pdf ME1_sample-exam-1.pdf ME1_sample-exam-1-solutions.pdf ME1_sample-exam-2.pdf ME1_sample-exam-2-solutions.pdf ME1_sample-exam-3.pdf ME1_sample-exam-3-solutions.pdf ME1_sample-exam-4.pdf ME1_sample-exam-4-solutions.pdf
Lecture 06: Statecharts	EN_05a_statecharts.pdf
Lecture 07: Modeling examples	EN_05c_modeling_example.pdf EN_05c_presented_models.zip
Lecture 08: Software model checking. Modelling example.	EN_06a_software_model_checking.pdf EN06b_The_Meltdown_modelling_example.pdf EN06b_The_Meltdown_modelling_example.zip
Lecture 09: Petri nets: Basic elements and extensions	EN_07a_PN_basic_elements_and_extensions.pdf
Lecture 10: Petri nets: Dynamic properties	EN_10a_PN_dynamic_properties.pdf EN_10b_PN_reduction.pdf
Lecture 11: Petri nets: Structural properties and modeling	Slides with white background are not part of the 2nd midterm exam. EN_11a_PN_structural_properties.pdf EN_11b_PN_modeling.pdf
Lecture 12: Hierarchical and Colored Petri nets	EN_12a_PN_hierarchical.pdf EN_12b_CPN.pdf
Lecture 13: Stochastic Petri nets	EN_13a_SPN.pdf
MIDTERM EXAM 2: Examples	ME2_sample-exam-1.pdf ME2_sample-exam-1-solutions.pdf ME2_sample-exam-2.pdf ME2_sample-exam-2-solutions.pdf

Félév: 2019. tavasz
Title	Egyedi szöveg
Lecture 01: Course overview, introduction	EN_01a_Course_overview.pdf EN_01b_role_of_formal_methods.pdf EN_01c_basic_formalisms.pdf EN_01d_SCADE_toolset.pdf (Optional material) Hyman example
Lecture 02: Temporal logics, LTL	EN_02a_linear_temporal_logic.pdf
Lecture 03: Temporal logics, CTL, CTL*	EN_02b_branching_time_temporal_logics.pdf
Lecture 04: Model checking	EN_03a_model_checking.pdf
Lecture 05: Efficient techniques for model checking	An online tool for building and visualizing ROBDDs: http://formal.cs.utah.edu:8080/pbl/BDD.php EN_04a_ROBDD_model checking.pdf EN_04b_bounded_model_checking.pdf
MIDTERM EXAM 1: Examples	ME1_sample-exam-1.pdf ME1_sample-exam-1-solutions.pdf ME1_sample-exam-2.pdf ME1_sample-exam-2-solutions.pdf ME1_sample-exam-3.pdf ME1_sample-exam-3-solutions.pdf ME1_sample-exam-4.pdf ME1_sample-exam-4-solutions.pdf
Lecture 06: Statecharts and practice	EN_06a_statecharts.pdf EN_06b_practice_examples.pdf
Lecture 07: Modeling examples	EN_06c_modeling_example.pdf Modeling-examples.zip
Lecture 08: Software model checking	EN_07a_software_model_checking.pdf EN_07b_cfa_examples.pdf
Lecture 09: Petri nets: Basic elements and extensions	EN_08a_PN_basic_elements_and_extensions.pdf