Lehekülje Software Synthesis and Verification lähteteksti vaatamine

'''Course code''': ITI8531 <br>
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br>

'''Lecturer''': prof. Jüri Vain <br>
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br>

'''Lab assistants''': 
Evelin Halling, Jishu Quin <br>
'''Contact''': evelin.halling ätt ttu.ee, <br>



Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]
<br>


==Time and place==

Lectures: Thursdays 10:00, ICT-A2 <br>
Labs: Thursdays 12:00, ICT-402 - Evelin Halling, Jishu Quin


<span style="color: red; font-weight: bold">'''Lab on March 16 will be cancelled due to the sickness of lab instructor.</span>.

==Lecture plan==
* [[Media:ITI8531_Lecture_1_16_intro.pdf|Lecture 1]]: Introduction
* [[Media:ITI8531_Lecture_2_17.pdf|Lecture 2]]: Modelling state transition systems
* [[Media:ITI8531_Lecture_3_17_CTL.pdf|Lecture 3]]: Temporal logic CTL*
* [[Media:ITI8531_Lecture_4_17_modelchecking.pdf|Lecture 4]]: CTL model checking
* [[Media:ITI8531_Lecture_5_17_TA_and_TCTL.pdf|Lecture 5]]: Timed automata and TCTL model checking
* Practicing for Test 1 (see Exercises 1 below)
* Test 1: Model checking ('''16.03.2017''')
** [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: Model checking
* [[Media:ITI8531_Lecture_5_16_Specifications.pdf|Lecture 7]]: Program specifications
* [[Media:ITI8531_synthesis1_2017.pdf|Lecture 8]]: Program synthesis I
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 9]]: Program synthesis II
* Test 2 (13.04.2017): Program synthesis
* [[Media:ITI8531_Lecture_6_16_rules.pdf|Lecture 11]]: Proving partial correctness of programs
* [[Media:ITI0130_lecture9_1_2015.pdf|Lecture 12.1]]: Proof techniques (1): derived rules, backwards proof, annotations
* [[Media:ITI0130_lecture9_2_2015.pdf|Lecture 12.2]]: Proof techniques (2): Array- and FOR-rule
* [[Media:ITI0130_lecture10_2015.pdf|Lecture 13]]: Proving total correctness of while-programs 
* Test 3 (05.05.2016): Deductive verification of sequential programs
* [[Media:ITI0130_lecture11_2015nondeterministic.pdf|Lecture 15]]: Non-deterministic programs
* [[Media:ITI0130_lecture_12_2015.pdf|Lecture 16]]: Parallel programs with shared variables
* [[Media:ITI0130_lecture_13_2015.pdf|Lecture 17]]: Parallel programs with message passing
* [[Media:ITI8531_lecture_14_2016.pdf|Lecture 18]]: Program synthesis
* Test 3 (26.05.2016): Deductive verification of non-deterministic and parallel programs

==Labs==
* Lab 1 -2: Introduction to modelling in UPPAAL 
** [http://www.uppaal.org/ UPPAAL website]
** [http://www.it.uu.se/research/group/darts/uppaal/small_tutorial.pdf Small tutorial on UPPAAL]
** [http://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf Tutorial on UPPAAL]
** Slides: [[Media:ITI0130_uppaal_eng_2013.pdf|UPPAAL introduction]]
** Model: [[Media:ITI0130_Light.xml|Lamp example]]
** Query: [[Media:ITI0130_Light.q|Lamp example]]
* Lab 3: Introduction to modelling in UPPAAL
** Assignment: Coffee Machine
** Slides: [[Media:ITI0130_Lab1_Coffee_machine_2015.pdf|Example and explanation]]
** Model: [[Media:ITI0130_Coffee.xml|Coffee machine]]
** Query: [[Media:ITI0130_Coffee.q|Coffee machine]]
* Lab 4: UPPAAL
** Assignment: Reader-Writer (unreliable) communication protocol
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]
* Lab 5: UPPAAL
** Assignment: Leader election protocol 
** Slides: [[Media:ITI0130_Lab3_IEEE1394.pdf|Explanation]]
** [http://perso.ens-lyon.fr/pierre.lescanne/ENSEIGNEMENT/REECRITURE/ABRIAL/sldp.ieee1394.pdf The Leader Election Protocol (IEEE 1394)]
** [http://link.springer.com/article/10.1023%2FA%3A1008764923992 Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394]
* Lab 6: UPPAAL
** Homework defenses

<!--
* Lab 7: KeY Introduction
** Installation: [[Media:ITI0130_Lab7_2016_KeY.pdf|KeY Installation]]
** Bank example: [[Media:ITI0130_Lab7_2016_Bank.zip|Bank example]]
** Bank JML: [[Media:ITI0130_Lab7_2016_Bank_JML.zip|Bank JML]]


* Lab 5: Design-by-Contract
** [https://github.com/nhatminhle/cofoja Contracts for Java (Cofoja)]
** [https://code.google.com/p/cofoja/w/list Cofoja wiki page]
** [[Media:ITI0130_Lab5_cofoja_setup.pdf|Installation instructions]]
** [[Media:ITI0130_Lab5_FM_cofoja.zip|Sample code]]

* Lab 6: Design-by-Contract
** [[Media:ITI0130_Lab5_db.zip|Database]]

* Lab 7: Design-by-Contract
** [[Media:ITI0130_Lab7_db2.zip|Secure Database]]

* Lab 8: Design-by-Contract
** [[Media:ITI0130_Lab7_assignment_cofoja.zip|Cofoja Assignment]]
*** [[Media:ITI0130_Lab7_assignment_Instruction.pdf|Instructions]]

* Lab 9: Key Tool
** [[Media:ITI0130_Lab8_Key_Instruction.pdf|Installation]]

* Lab 10: Key Tool
** [[Media:ITI0130_Lab9_Key_practise.zip|Key Examples]]

* Lab 11: Key Tool
** [[Media:ITI0130_Lab11_Key_practise.zip|JML]]
** [[Media:ITI0130_Lab11_summax.zip|SumAndMax Example]]

* Lab 12: Key Tool
** [[Media:ITI0130_Lab12_Key_assignment.zip|Key assignment]]

* Lab 13: Key Tool
** [[Media:ITI0130_Lab13_Bank_example_solution.zip|Solution to Bank example]]
-->

== Exercises==
* [[Media:Test 1_2017for practicing.pdf|Exercises 1]]: Model checking (explicit and symbolic state)
* [[Media:Exercises_2.pdf|Exercises 2]]: Partial correctness of WHILE-programs
** [[Media:while_program_example_2015.pdf|Example 1]]: Partial correctness of WHILE-loop
** [[Media:DEDUCTIVE_VERIFICATION_Example_2.pdf|Example 2]]: Partial correctness of FOR-loop
* Partial correctness of non-deterministic and parallel programs
** [[Media:Exercises__3.pdf|Exercises 3.1]]: Partial correctness of non-deterministic and parallel programs
** [[Media:Test3_exercises_solutions.pdf|Exercises 3.2]]: Partial correctness of non-deterministic and parallel programs NEW!!!

==Resources==
* [http://www.fmeurope.org/ Formal Methods Europe]
* [[Media: 1st_order_proof_rules.pdf|Genzen's proof system for 1st order logic]]: 
* [[Media: Proof_rules_of_Hoare_logic.pdf|HL proof rules for sequential and parallel programs]]:
* [[Media: Invariants.pdf|Some guidlines how to find invariants]]
* Mike Gordon's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]