http://courses.cs.taltech.ee/w/api.php?action=feedcontributions&feedformat=atom&user=DeepakPal Kursused - Kasutaja kaastöö [et] 2026-04-09T11:09:09Z Kasutaja kaastöö MediaWiki 1.35.9 http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6727 Software Synthesis and Verification 2018-05-13T07:24:35Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_18_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_18_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_18_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;15.03.2018&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 7.1]]: Program specifications<br /> * [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7.2]]: Proving partial correctness of programs<br /> * [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Practicing for Test 2 (26.04.2018): Deductive verification of non-deterministic and parallel programs<br /> ** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br /> * Test 2 (03.05.2018, 12.00): Deductive verification of sequential, non-deterministic and parallel programs<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 3 (17.05.2018): Program synthesis<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Jobber.xml|JobShop Model with three possible scenarios]]<br /> ** Query: [[Media:Jobber_Query1.q|JobShop Query]]<br /> <br /> * Lab 4-5: Implementation of Mutual Exclusion Algorithms in UPPAAL <br /> ** Slides: [[Media:Lecture_5.pdf|The Mutual Exclusion Problem and Algorithms]]<br /> ** Model: [[Media:Attempt1_Model.xml|First Attempt Algorithm Model]]<br /> ** Query: [[Media:Attempt1_query.q|First Attempt Query]]<br /> <br /> * Lab 6: Lab Assignment: ATM System, JobShop, Implementation of Mutual Exclusion Algo. <br /> ** Slides: [[Media:Lab_Assignments.pdf|Tasks and explanation]]<br /> <br /> * Lab 7-8: Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> <br /> * Lab 9: Assignment: Elevator Control<br /> ** Slides: [[Media:ElevatorControl_V1_29062017.pdf|Example and explanation]]<br /> ** Slides: [[Media:ModellingRequirement.pptx|Modelling Requirements]]<br /> <br /> * Lab 10: Final Assessment on 17 May 2018<br /> ** Lab defending of all given assignment.<br /> <br /> &lt;!--<br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> <br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6726 Software Synthesis and Verification 2018-05-13T07:23:43Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_18_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_18_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_18_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;15.03.2018&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 7.1]]: Program specifications<br /> * [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7.2]]: Proving partial correctness of programs<br /> * [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Practicing for Test 2 (26.04.2018): Deductive verification of non-deterministic and parallel programs<br /> ** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br /> * Test 2 (03.05.2018, 12.00): Deductive verification of sequential, non-deterministic and parallel programs<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 3 (17.05.2018): Program synthesis<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Jobber.xml|JobShop Model with three possible scenarios]]<br /> ** Query: [[Media:Jobber_Query1.q|JobShop Query]]<br /> <br /> * Lab 4-5: Implementation of Mutual Exclusion Algorithms in UPPAAL <br /> ** Slides: [[Media:Lecture_5.pdf|The Mutual Exclusion Problem and Algorithms]]<br /> ** Model: [[Media:Attempt1_Model.xml|First Attempt Algorithm Model]]<br /> ** Query: [[Media:Attempt1_query.q|First Attempt Query]]<br /> <br /> * Lab 6: Lab Assignment: ATM System, JobShop, Implementation of Mutual Exclusion Algo. <br /> ** Slides: [[Media:Lab_Assignments.pdf|Tasks and explanation]]<br /> <br /> * Lab 7-8: Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> <br /> * Lab 9: Assignment: Elevator Control<br /> ** Slides: [[Media:ElevatorControl_V1_29062017.pdf|Example and explanation]]<br /> ** Slides: [[Media:ModellingRequirement.pptx|Modelling Requirements]]<br /> <br /> * Lab 10: Final Assessment<br /> ** Lab defending of all given assignment.<br /> <br /> &lt;!--<br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> <br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6629 Software Synthesis and Verification 2018-04-15T19:16:16Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_18_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_18_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_18_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;15.03.2018&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 7.1]]: Program specifications<br /> * [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7.2]]: Proving partial correctness of programs<br /> * [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 2 (26.04.2018): Deductive verification of non-deterministic and parallel programs<br /> ** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br /> <br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 3 (13.04.2017): Program synthesis<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Jobber.xml|JobShop Model with three possible scenarios]]<br /> ** Query: [[Media:Jobber_Query1.q|JobShop Query]]<br /> <br /> * Lab 4-5: Implementation of Mutual Exclusion Algorithms in UPPAAL <br /> ** Slides: [[Media:Lecture_5.pdf|The Mutual Exclusion Problem and Algorithms]]<br /> ** Model: [[Media:Attempt1_Model.xml|First Attempt Algorithm Model]]<br /> ** Query: [[Media:Attempt1_query.q|First Attempt Query]]<br /> <br /> * Lab 6: Lab Assignment: ATM System, JobShop, Implementation of Mutual Exclusion Algo. <br /> ** Slides: [[Media:Lab_Assignments.pdf|Tasks and explanation]]<br /> <br /> * Lab 7-8: Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> <br /> * Lab 9: Assignment: Elevator Control<br /> ** Slides: [[Media:ElevatorControl_V1_29062017.pdf|Example and explanation]]<br /> ** Slides: [[Media:ModellingRequirement.pptx|Modelling Requirements]]<br /> <br /> &lt;!--<br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> <br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:ModellingRequirement.pptx&diff=6628 Fail:ModellingRequirement.pptx 2018-04-15T19:14:12Z <p>DeepakPal: </p> <hr /> <div></div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6627 Software Synthesis and Verification 2018-04-15T19:12:58Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_18_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_18_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_18_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;15.03.2018&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 7.1]]: Program specifications<br /> * [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7.2]]: Proving partial correctness of programs<br /> * [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 2 (26.04.2018): Deductive verification of non-deterministic and parallel programs<br /> ** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br /> <br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 3 (13.04.2017): Program synthesis<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Jobber.xml|JobShop Model with three possible scenarios]]<br /> ** Query: [[Media:Jobber_Query1.q|JobShop Query]]<br /> <br /> * Lab 4-5: Implementation of Mutual Exclusion Algorithms in UPPAAL <br /> ** Slides: [[Media:Lecture_5.pdf|The Mutual Exclusion Problem and Algorithms]]<br /> ** Model: [[Media:Attempt1_Model.xml|First Attempt Algorithm Model]]<br /> ** Query: [[Media:Attempt1_query.q|First Attempt Query]]<br /> <br /> * Lab 6: Lab Assignment: ATM System, JobShop, Implementation of Mutual Exclusion Algo. <br /> ** Slides: [[Media:Lab_Assignments.pdf|Tasks and explanation]]<br /> <br /> * Lab 7-8: Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> <br /> * Lab 9: Assignment: Elevator Control<br /> ** Slides: [[Media:ElevatorControl_V1_29062017.pdf|Example and explanation]]<br /> <br /> &lt;!--<br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> <br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:ElevatorControl_V1_29062017.pdf&diff=6626 Fail:ElevatorControl V1 29062017.pdf 2018-04-15T19:12:23Z <p>DeepakPal: </p> <hr /> <div></div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6556 Software Synthesis and Verification 2018-03-29T06:35:43Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_18_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Jobber.xml|JobShop Model with three possible scenarios]]<br /> ** Query: [[Media:Jobber_Query1.q|JobShop Query]]<br /> <br /> * Lab 4-5: Implementation of Mutual Exclusion Algorithms in UPPAAL <br /> ** Slides: [[Media:Lecture_5.pdf|The Mutual Exclusion Problem and Algorithms]]<br /> ** Model: [[Media:Attempt1_Model.xml|First Attempt Algorithm Model]]<br /> ** Query: [[Media:Attempt1_query.q|First Attempt Query]]<br /> <br /> * Lab 6: Lab Assignment: ATM System, JobShop, Implementation of Mutual Exclusion Algo. <br /> ** Slides: [[Media:Lab_Assignments.pdf|Tasks and explanation]]<br /> <br /> * Lab 7-8: Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> <br /> &lt;!--<br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> <br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6555 Software Synthesis and Verification 2018-03-29T06:23:25Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_18_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Jobber.xml|JobShop Model with three possible scenarios]]<br /> ** Query: [[Media:Jobber_Query1.q|JobShop Query]]<br /> <br /> * Lab 4-5: Implementation of Mutual Exclusion Algorithms in UPPAAL <br /> ** Slides: [[Media:Lecture_5.pdf|The Mutual Exclusion Problem and Algorithms]]<br /> ** Model: [[Media:Attempt1_Model.xml|First Attempt Algorithm Model]]<br /> ** Query: [[Media:Attempt1_query.q|First Attempt Query]]<br /> <br /> * Lab Assignment: ATM System, JobShop, Implementation of Mutual Exclusion Algo. <br /> ** Slides: [[Media:Lab_Assignments.pdf|Tasks and explanation]]<br /> <br /> <br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 5: Assignment 2: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6500 Software Synthesis and Verification 2018-03-08T17:12:07Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_18_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Jobber.xml|JobShop Model with three possible scenarios]]<br /> ** Query: [[Media:Jobber_Query1.q|JobShop Query]]<br /> <br /> * Lab 4-5: Implementation of Mutual Exclusion Algorithms in UPPAAL <br /> ** Slides: [[Media:Lecture_5.pdf|The Mutual Exclusion Problem and Algorithms]]<br /> ** Model: [[Media:Attempt1_Model.xml|First Attempt Algorithm Model]]<br /> ** Query: [[Media:Attempt1_query.q|First Attempt Query]]<br /> <br /> * Lab Assignment: ATM System, JobShop, Implementation of Mutual Exclusion Algo. <br /> ** Slides: [[Media:Lab_Assignments.pdf|Tasks and explanation]]<br /> <br /> &lt;!--<br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 5: Assignment 2: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> <br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:Lab_Assignments.pdf&diff=6499 Fail:Lab Assignments.pdf 2018-03-08T17:10:40Z <p>DeepakPal: </p> <hr /> <div></div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6498 Software Synthesis and Verification 2018-03-08T15:46:20Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_18_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Jobber.xml|JobShop Model with three possible scenarios]]<br /> ** Query: [[Media:Jobber_Query1.q|JobShop Query]]<br /> <br /> * Lab 4-5: Implementation of Mutual Exclusion Algorithms in UPPAAL <br /> ** Slides: [[Media:Lecture_5.pdf|The Mutual Exclusion Problem and Algorithms]]<br /> ** Model: [[Media:Attempt1_Model.xml|First Attempt Algorithm Model]]<br /> ** Query: [[Media:Attempt1_query.q|First Attempt Query]]<br /> <br /> &lt;!--<br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 5: Assignment 2: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> <br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6497 Software Synthesis and Verification 2018-03-08T15:44:28Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_18_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Jobber.xml|JobShop Model with three possible scenarios]]<br /> ** Query: [[Media:Jobber_Query1.q|JobShop Query]]<br /> <br /> * Lab 4-5: Implementation of Mutual Exclusion Algorithms in UPPAAL <br /> ** Slides: [[Media:Lecture_5.pdf|The Mutual Exclusion Problem and Algorithms]]<br /> ** Model: [[Media:Attempt1_Model.xml|First Attempt Algorithm Model]]<br /> ** Query: [[Media:Attempt1_query.q|First Attempt Query]]<br /> <br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 5: Assignment 2: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:Attempt1_query.q&diff=6496 Fail:Attempt1 query.q 2018-03-08T15:44:03Z <p>DeepakPal: </p> <hr /> <div></div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:Attempt1_Model.xml&diff=6495 Fail:Attempt1 Model.xml 2018-03-08T15:42:55Z <p>DeepakPal: </p> <hr /> <div></div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:Lecture_5.pdf&diff=6494 Fail:Lecture 5.pdf 2018-03-08T15:37:49Z <p>DeepakPal: </p> <hr /> <div></div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6444 Software Synthesis and Verification 2018-02-22T22:11:01Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_18_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Jobber.xml|JobShop Model with three possible scenarios]]<br /> ** Query: [[Media:Jobber_Query1.q|JobShop Query]]<br /> <br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 5: Assignment 2: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:Jobber_Query1.q&diff=6443 Fail:Jobber Query1.q 2018-02-22T22:10:46Z <p>DeepakPal: </p> <hr /> <div></div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6442 Software Synthesis and Verification 2018-02-22T22:09:09Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_18_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Jobber.xml|JobShop Model with three possible scenarios]]<br /> ** Query: [[Media:Jobber_query.q|JobShop Query]]<br /> <br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 5: Assignment 2: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6441 Software Synthesis and Verification 2018-02-22T22:08:31Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_18_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Jobber.xml|JobShop Model with three possible scenarios]]<br /> ** Query: [[Media:Jobber_query.q|JobShop Query<br /> <br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 5: Assignment 2: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:Jobber_query.q&diff=6440 Fail:Jobber query.q 2018-02-22T22:08:17Z <p>DeepakPal: </p> <hr /> <div></div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:Jobber.xml&diff=6439 Fail:Jobber.xml 2018-02-22T22:06:37Z <p>DeepakPal: </p> <hr /> <div></div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6435 Software Synthesis and Verification 2018-02-22T07:20:05Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:|JobShop Model]]<br /> ** Query: [[Media:|JobShop Query<br /> <br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 5: Assignment 2: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6434 Software Synthesis and Verification 2018-02-22T07:19:14Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:|ATM System Model]]<br /> ** Query: [[Media:|ATM System Query]]<br /> <br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 5: Assignment 2: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6433 Software Synthesis and Verification 2018-02-22T07:11:03Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:Lab3_Lab_Lecture.pdf|Uppaal Modelling Language]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 5: Assignment 2: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:Lab3_Lab_Lecture.pdf&diff=6432 Fail:Lab3 Lab Lecture.pdf 2018-02-22T07:08:56Z <p>DeepakPal: </p> <hr /> <div></div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6431 Software Synthesis and Verification 2018-02-22T07:08:26Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Understanding of Clocks and State Space Explosion in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 4: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 5: Assignment 2: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 6: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 7: Lab Exam<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6430 Software Synthesis and Verification 2018-02-22T07:05:47Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Assignment 1: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 4: Assignment 2: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 5: Assignment 3: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 6: Lab Exam<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6429 Software Synthesis and Verification 2018-02-22T07:04:38Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Assignment 1<br /> ** Assignment: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 4: Assignment 2<br /> ** Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 5: Assignment 3<br /> ** Assignment: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 6: Lab Exam<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6428 Software Synthesis and Verification 2018-02-22T07:02:32Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:New_Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Introduction to modelling in UPPAAL<br /> ** Assignment: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 4: UPPAAL<br /> ** Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 5: UPPAAL<br /> ** Assignment: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 6: UPPAAL<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:New_Lab2_MODEL_CHECKING.pdf&diff=6427 Fail:New Lab2 MODEL CHECKING.pdf 2018-02-22T07:01:39Z <p>DeepakPal: </p> <hr /> <div></div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6426 Software Synthesis and Verification 2018-02-22T06:58:38Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 2: Validation (simulation) and verification (automatic model-checking) in UPPAAL <br /> ** Slides: [[Media:Lab2_MODEL_CHECKING.pdf|Model Checking introduction]]<br /> ** Model: [[Media:Atm_system.xml|ATM System Model]]<br /> ** Query: [[Media:Atm_system_query.q|ATM System Query]]<br /> <br /> * Lab 3: Introduction to modelling in UPPAAL<br /> ** Assignment: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 4: UPPAAL<br /> ** Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 5: UPPAAL<br /> ** Assignment: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 6: UPPAAL<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:Atm_system_query.q&diff=6425 Fail:Atm system query.q 2018-02-22T06:58:25Z <p>DeepakPal: </p> <hr /> <div></div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:Atm_system.xml&diff=6424 Fail:Atm system.xml 2018-02-22T06:57:53Z <p>DeepakPal: ATM_Model</p> <hr /> <div>ATM_Model</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:Lab2_MODEL_CHECKING.pdf&diff=6423 Fail:Lab2 MODEL CHECKING.pdf 2018-02-22T06:57:18Z <p>DeepakPal: Model_Checking_Theory</p> <hr /> <div>Model_Checking_Theory</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6422 Software Synthesis and Verification 2018-02-22T06:47:07Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 3: Introduction to modelling in UPPAAL<br /> ** Assignment: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 4: UPPAAL<br /> ** Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 5: UPPAAL<br /> ** Assignment: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 6: UPPAAL<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6421 Software Synthesis and Verification 2018-02-22T06:43:52Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> For More reading, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 3: Introduction to modelling in UPPAAL<br /> ** Assignment: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 4: UPPAAL<br /> ** Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 5: UPPAAL<br /> ** Assignment: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 6: UPPAAL<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6420 Software Synthesis and Verification 2018-02-22T06:42:58Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More Reading about Uppaal, refer below links:<br /> *** [http://www.uppaal.org/ UPPAAL website]<br /> *** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> *** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 3: Introduction to modelling in UPPAAL<br /> ** Assignment: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 4: UPPAAL<br /> ** Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 5: UPPAAL<br /> ** Assignment: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 6: UPPAAL<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6419 Software Synthesis and Verification 2018-02-22T06:42:01Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** For More Reading about Uppaal, refer below links:<br /> ** [http://www.uppaal.org/ UPPAAL website]<br /> ** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> ** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 3: Introduction to modelling in UPPAAL<br /> ** Assignment: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 4: UPPAAL<br /> ** Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 5: UPPAAL<br /> ** Assignment: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 6: UPPAAL<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6418 Software Synthesis and Verification 2018-02-22T06:37:54Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:LightController.xml|Light Controller Model]]<br /> ** Query: [[Media:LightControllerQuery.q|Light Controller Query]]<br /> ** [http://www.uppaal.org/ UPPAAL website]<br /> ** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> ** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 3: Introduction to modelling in UPPAAL<br /> ** Assignment: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 4: UPPAAL<br /> ** Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 5: UPPAAL<br /> ** Assignment: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 6: UPPAAL<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:LightControllerQuery.q&diff=6417 Fail:LightControllerQuery.q 2018-02-22T06:37:33Z <p>DeepakPal: Light Controller Query</p> <hr /> <div>Light Controller Query</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:LightController.xml&diff=6416 Fail:LightController.xml 2018-02-22T06:35:38Z <p>DeepakPal: Light Controller Model</p> <hr /> <div>Light Controller Model</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6415 Software Synthesis and Verification 2018-02-22T06:32:06Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:UPPAAL Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:ITI0130_Light.xml|Lamp example]]<br /> ** Query: [[Media:ITI0130_Light.q|Lamp example]]<br /> ** [http://www.uppaal.org/ UPPAAL website]<br /> ** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> ** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 3: Introduction to modelling in UPPAAL<br /> ** Assignment: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 4: UPPAAL<br /> ** Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 5: UPPAAL<br /> ** Assignment: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 6: UPPAAL<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:UPPAAL_Tutorial.pdf&diff=6414 Fail:UPPAAL Tutorial.pdf 2018-02-22T06:30:09Z <p>DeepakPal: DeepakPal laadis üles faili &amp;quot;Pilt:UPPAAL Tutorial.pdf&amp;quot; uue versiooni</p> <hr /> <div>UPPAAL introduction</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=6413 Software Synthesis and Verification 2018-02-22T06:25:52Z <p>DeepakPal: /* Labs */</p> <hr /> <div>&#039;&#039;&#039;Course code&#039;&#039;&#039;: ITI8531 &lt;br&gt;<br /> &#039;&#039;&#039;Link&#039;&#039;&#039;: http://courses.cs.ttu.ee/pages/ITI0130&lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lecturer&#039;&#039;&#039;: prof. Jüri Vain &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: juri.vain ätt ttu.ee, ICT-418 &lt;br&gt;<br /> <br /> &#039;&#039;&#039;Lab assistant&#039;&#039;&#039;: <br /> Deepak Pal &lt;br&gt;<br /> &#039;&#039;&#039;Contact&#039;&#039;&#039;: deepak.pal ätt ttu.ee, &lt;br&gt;<br /> <br /> <br /> <br /> Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br /> &lt;br&gt;<br /> <br /> <br /> ==Time and place==<br /> <br /> Lectures: Thursdays 10:00, ICT-A1 &lt;br&gt;<br /> Labs: Thursdays 12:00, ICT-122 - Deepak Pal<br /> <br /> &#039;&#039;&#039;New!&#039;&#039;&#039;&lt;br&gt;<br /> &#039;&#039;&#039;Exams: &#039;&#039;&#039;<br /> * Thursday May 1, 10:00, room ICT-A2 &lt;br&gt;<br /> * Thursday May 8, 10:00, room ICT-A2&#039;&#039;&#039;<br /> <br /> ==Lecture plan==<br /> * [[Media:ITI8531_Lecture_1_18_Intro.pdf|Lecture 1]]: Introduction<br /> * [[Media:ITI8531_Lecture_2_18_transition_systems.pdf|Lecture 2]]: Modelling state transition systems<br /> * [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*<br /> * [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking<br /> * [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking<br /> * Practicing for Test 1 (see Exercises 1 below)<br /> * Test 1: Model checking (&#039;&#039;&#039;16.03.2017&#039;&#039;&#039;)<br /> ** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking<br /> * [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications<br /> * [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I<br /> * [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II<br /> * Test 2 (13.04.2017): Program synthesis<br /> * [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs<br /> * [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations<br /> * [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule<br /> * [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs <br /> * [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 14]]: Verifying nondeterministic and parallel programs<br /> * Test 3 (25.05.2017): Deductive verification of non-deterministic and parallel programs<br /> <br /> ==Labs==<br /> * Lab 1: Introduction to modelling in UPPAAL <br /> ** Slides: [[Media:Lab1_UPPAAL_Tutorial.pdf|UPPAAL introduction]]<br /> ** Model: [[Media:ITI0130_Light.xml|Lamp example]]<br /> ** Query: [[Media:ITI0130_Light.q|Lamp example]]<br /> ** [http://www.uppaal.org/ UPPAAL website]<br /> ** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]<br /> ** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]<br /> <br /> * Lab 3: Introduction to modelling in UPPAAL<br /> ** Assignment: Coffee Machine<br /> ** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]<br /> ** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]<br /> ** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]<br /> * Lab 4: UPPAAL<br /> ** Assignment: Reader-Writer (unreliable) communication protocol<br /> ** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br /> * Lab 5: UPPAAL<br /> ** Assignment: Leader election protocol <br /> ** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]<br /> ** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]<br /> ** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]<br /> ** Reference solution: [[Media:FASDS.pdf|Chapter 12]]<br /> * Lab 6: UPPAAL<br /> ** Homework defenses<br /> <br /> &lt;!--<br /> * Lab 7: KeY Introduction<br /> ** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]<br /> ** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]<br /> ** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]<br /> <br /> <br /> * Lab 5: Design-by-Contract<br /> ** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]<br /> ** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]<br /> ** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]<br /> ** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]<br /> <br /> * Lab 6: Design-by-Contract<br /> ** [[Media:ITI0130_Lab5_db.zip|Database]]<br /> <br /> * Lab 7: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]<br /> <br /> * Lab 8: Design-by-Contract<br /> ** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]<br /> *** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]<br /> <br /> * Lab 9: Key Tool<br /> ** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]<br /> <br /> * Lab 10: Key Tool<br /> ** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]<br /> <br /> * Lab 11: Key Tool<br /> ** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]<br /> ** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]<br /> <br /> * Lab 12: Key Tool<br /> ** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]<br /> <br /> * Lab 13: Key Tool<br /> ** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]<br /> --&gt;<br /> <br /> == Exercises==<br /> * [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)<br /> * [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs<br /> ** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop<br /> ** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop<br /> * Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs<br /> ** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs <br /> ** [[Media:Harjutused_3.pdf|Exercises 3.3]]: Parallel programs with message passing<br /> <br /> ==Resources==<br /> * [http://www.fmeurope.org/ Formal Methods Europe]<br /> * [[Media: 1st_order_proof_rules.pdf|Genzen&#039;s proof system for 1st order logic]]: <br /> * [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:<br /> * [[Media: Invariants.pdf|Some guidlines how to find invariants]]<br /> * Mike Gordon&#039;s lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div> DeepakPal http://courses.cs.taltech.ee/w/index.php?title=Fail:UPPAAL_Tutorial.pdf&diff=6412 Fail:UPPAAL Tutorial.pdf 2018-02-22T06:15:54Z <p>DeepakPal: UPPAAL introduction</p> <hr /> <div>UPPAAL introduction</div> DeepakPal