http://courses.cs.taltech.ee/w/api.php?action=feedcontributions&feedformat=atom&user=Leonidas
Kursused - Kasutaja kaastöö [et]
2026-04-09T12:54:34Z
Kasutaja kaastöö
MediaWiki 1.35.9
http://courses.cs.taltech.ee/w/index.php?title=MSc_seminar_I_2022_Spring&diff=10366
MSc seminar I 2022 Spring
2022-01-24T12:39:39Z
<p>Leonidas: /* ITX8301 Magistriseminar I / MSc Seminar I */</p>
<hr />
<div>=ITX8301 Magistriseminar I / MSc Seminar I=<br />
<br />
Lecturer:<br />
<br />
* [https://taltech.ee/en/contacts/leonidas-tsiopoulos Leonidas Tsiopoulos]<br />
<br />
Spring 2022: Tue 16:00-17:30 online only in [[https://teams.microsoft.com/l/team/19%3aP-pCq0TTDVLM5QVHFU_TQSDIHGniNlT4yGleTW-fIPQ1%40thread.tacv2/conversations?groupId=a2f03dce-0a9b-4697-b178-8224243b0abe&tenantId=3efd4d88-9b88-4fc9-b6c0-c7ca50f1db57 MS Teams Team for ITX8301 in Spring 2022]].<br />
<br />
Preliminary plan:<br />
* Jan 25: Introduction. How to perform search and evaluate sources I<br />
[https://scholar.google.com Google Scholar], [https://dblp.uni-trier.de DBLP], [https://www.taltech.ee/en/library Tallinn University of Technology Library], [https://digikogu.taltech.ee/en/Search/Items?ItemTypes=18&ItemTypes=9&ItemTypes=19&Query%914%93=&Query%915%93=&Query%918%93=&Query%917%93=IVSM Theses defended in Software Engineering MSc in Tallinn University of Technology]. To access the research papers in various portals, please consider using [https://confluence.ttu.ee/it-info/it-arvuti-ja-oppetoeoekoht/kauguehendus-vpn/kaugtoeoeuehendus-eduvpn EduVPN]<br />
<br />
* Feb 1: How to perform search and evaluate sources II. <br />
<br />
* Task: deadline March 1: Pick a research paper (with the help of supervisor / seminar lecturer), read it and be prepared to present the results.<br />
<br />
* Feb 8 - Discussion on how research papers are written and how to read them. Please watch the following video before the seminar: [https://www.microsoft.com/en-us/research/academic-program/write-great-research-paper/]<br />
* Feb 15 Research talks by example. Please watch some talk videos, e.g. [https://esec-fse19.ut.ee/program/keynotes/ ESEC/FSE2019 keynotes] [https://www.youtube.com/watch?v=vgdVIeQKH-E Satya Nadella's keynote at CVPR2020] (Current videos from the CVF youtube channel [https://www.youtube.com/channel/UC0n76gicaarsN_Y9YShWwhw]) (more links to be provided according to your interests).<br />
* Feb 22 Discussion on how to give research talks. Please watch the video ahead of the seminar [https://www.microsoft.com/en-us/research/academic-program/give-great-research-talk/]<br />
* March 1: Student presentations round I (research paper of interest or problem statement, 20 min presentation)<br />
<br />
* March 8: Student presentations round I (research paper of interest or problem statement, 20 min presentation)<br />
<br />
* March 15: Student presentations round I (research paper of interest or problem statement, 20 min presentation) <br />
<br />
* March 22 : Student presentations round I (additional slot) (research paper of interest or problem statement, 20 min presentation)<br />
<br />
* March 29: What constitutes a good [[Problem Statement]] for MSc thesis? <br />
* April 5: Interactive session on planned problem statements<br />
* April 12: Structured writing in Latex<br />
* April 19: Discussion of submissions (submissions due on April 30)<br />
* April 26: Student presentations II<br />
**<br />
**<br />
**<br />
**<br />
* May 3: Student presentations II<br />
<br />
**<br />
* May 10: Student presentations II<br />
<br />
<br />
<br />
== Student presentations ==<br />
<br />
On your MSc topic<br />
<br />
April - May<br />
<br />
<br />
The discussions in Teams.<br />
<br />
== Thesis topics ==<br />
<br />
[https://cs.ttu.ee/services/protsessor|List of thesis topics for defence]<br />
<br />
== Methods for research ==<br />
<br />
[[Selecting the Research Method]]<br />
<br />
= Grading =<br />
<br />
==ITX8301:==<br />
<br />
* 50% Written problem statement.<br />
* 20% Presentation of research paper (peresentation session I).<br />
* 30% Final presentation and participation in sessions where fellow students give presentations.<br />
<br />
==ITX8302:==<br />
<br />
* 20% of 100%: Problem statement and methodology.<br />
* 50% of 100%: Written background and related work submission.<br />
* 30% of 100%: Your mock defence talk and participation in seminars where other students give talks. Note that you will need to submit your current draft of the thesis by the time you give the talk. The draft is not marked, but it will be used for questions after your talk. <br />
<br />
The final grade will be calculated as follows from the sum of the above results:<br />
<br />
* 90% or more: 5<br />
* 80% or more: 4<br />
* 70% or more: 3<br />
* 60% or more: 2<br />
* 50% or more: 1<br />
* less than 50%: 0</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=MSc_seminar_I_2022_Spring&diff=10365
MSc seminar I 2022 Spring
2022-01-24T12:34:37Z
<p>Leonidas: /* ITX8301 Magistriseminar I / MSc Seminar I */</p>
<hr />
<div>=ITX8301 Magistriseminar I / MSc Seminar I=<br />
<br />
Lecturer:<br />
<br />
* [https://taltech.ee/en/contacts/leonidas-tsiopoulos Leonidas Tsiopoulos]<br />
<br />
Spring 2022: Tue 16:00-17:30 online only in [[https://teams.microsoft.com/l/team/19%3aP-pCq0TTDVLM5QVHFU_TQSDIHGniNlT4yGleTW-fIPQ1%40thread.tacv2/conversations?groupId=a2f03dce-0a9b-4697-b178-8224243b0abe&tenantId=3efd4d88-9b88-4fc9-b6c0-c7ca50f1db57 MS Teams Team for ITX8301 in Spring 2022]].<br />
<br />
Preliminary plan:<br />
* Jan 25: Introduction. How to perform search and evaluate sources I<br />
[https://scholar.google.com Google Scholar], [https://academic.microsoft.com Microsoft Academic Search], [https://dblp.uni-trier.de DBLP], [https://www.taltech.ee/en/library Tallinn University of Technology Library], [https://digikogu.taltech.ee/en/Search/Items?ItemTypes=18&ItemTypes=9&ItemTypes=19&Query%914%93=&Query%915%93=&Query%918%93=&Query%917%93=IVSM Theses defended in Software Engineering MSc in Tallinn University of Technology]. To access the research papers in various portals, please consider using [https://confluence.ttu.ee/it-info/it-arvuti-ja-oppetoeoekoht/kauguehendus-vpn/kaugtoeoeuehendus-eduvpn EduVPN]<br />
<br />
* Feb 1: How to perform search and evaluate sources II. <br />
<br />
* Task: deadline March 1: Pick a research paper (with the help of supervisor / seminar lecturer), read it and be prepared to present the results.<br />
<br />
* Feb 8 - Discussion on how research papers are written and how to read them. Please watch the following video before the seminar: [https://www.microsoft.com/en-us/research/academic-program/write-great-research-paper/]<br />
* Feb 15 Research talks by example. Please watch some talk videos, e.g. [https://esec-fse19.ut.ee/program/keynotes/ ESEC/FSE2019 keynotes] [https://www.youtube.com/watch?v=vgdVIeQKH-E Satya Nadella's keynote at CVPR2020] (Current videos from the CVF youtube channel [https://www.youtube.com/channel/UC0n76gicaarsN_Y9YShWwhw]) (more links to be provided according to your interests).<br />
* Feb 22 Discussion on how to give research talks. Please watch the video ahead of the seminar [https://www.microsoft.com/en-us/research/academic-program/give-great-research-talk/]<br />
* March 1: Student presentations round I (research paper of interest or problem statement, 20 min presentation)<br />
<br />
* March 8: Student presentations round I (research paper of interest or problem statement, 20 min presentation)<br />
<br />
* March 15: Student presentations round I (research paper of interest or problem statement, 20 min presentation) <br />
<br />
* March 22 : Student presentations round I (additional slot) (research paper of interest or problem statement, 20 min presentation)<br />
<br />
* March 29: What constitutes a good [[Problem Statement]] for MSc thesis? <br />
* April 5: Interactive session on planned problem statements<br />
* April 12: Structured writing in Latex<br />
* April 19: Discussion of submissions (submissions due on April 30)<br />
* April 26: Student presentations II<br />
**<br />
**<br />
**<br />
**<br />
* May 3: Student presentations II<br />
<br />
**<br />
* May 10: Student presentations II<br />
<br />
<br />
<br />
== Student presentations ==<br />
<br />
On your MSc topic<br />
<br />
April - May<br />
<br />
<br />
The discussions in Teams.<br />
<br />
== Thesis topics ==<br />
<br />
[https://cs.ttu.ee/services/protsessor|List of thesis topics for defence]<br />
<br />
== Methods for research ==<br />
<br />
[[Selecting the Research Method]]<br />
<br />
= Grading =<br />
<br />
==ITX8301:==<br />
<br />
* 50% Written problem statement.<br />
* 20% Presentation of research paper (peresentation session I).<br />
* 30% Final presentation and participation in sessions where fellow students give presentations.<br />
<br />
==ITX8302:==<br />
<br />
* 20% of 100%: Problem statement and methodology.<br />
* 50% of 100%: Written background and related work submission.<br />
* 30% of 100%: Your mock defence talk and participation in seminars where other students give talks. Note that you will need to submit your current draft of the thesis by the time you give the talk. The draft is not marked, but it will be used for questions after your talk. <br />
<br />
The final grade will be calculated as follows from the sum of the above results:<br />
<br />
* 90% or more: 5<br />
* 80% or more: 4<br />
* 70% or more: 3<br />
* 60% or more: 2<br />
* 50% or more: 1<br />
* less than 50%: 0</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=9121
Software Synthesis and Verification
2020-02-14T08:47:31Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lecturer''': Leonidas Tsiopoulos <br><br />
'''Contact''': leonidas.tsiopoulos ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lecturer''': Maksym Bortin <br><br />
'''Contact''': maksym.bortin ätt ttu.ee, room B404 in the Cybernetics Building <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 10:00, ICT-341 <br><br />
Labs: Tuesdays 12:00, ICT-341 - Evelin Halling<br />
<br />
<br />
'''New!'''<br><br />
'''Exams: (To Be Updated) '''<br />
* ... <br><br />
** Exam is for those who have not passed any of the tests or want to improve their final mark<br />
<!--* ... '''<br />
<br />
--><br />
<br />
==Lecture plan - To be updated for Module II and III==<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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis with Acacia part III - Lecture 14.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:Software Synthesis - Lecture V - Recap.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<br />
* Retake of Test 2, 2nd task: ('''21.05.2019 at 12.00 (New!)''')<br />
** [[Media:Test_2_2019_lahendus.pdf|Eample_Solution]]: ('''Example solution of Task2 (NEW!)''')<br />
<br />
==Labs - To be updated from lab 4 onwards==<br />
* Exercise Environment for Module II:<br />
** Download and install the environment: [[Media:HoareLogic.tar| Hoare Logic environment]]<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 13:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
* Lab 14:<br />
** [[Media:ITI8531_LTL_exercises.pdf|Exercises]]<br />
** [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL tool]<br />
** [http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA]<br />
* Lab 15<br />
** [[Media:ITI8531_LTL_assignments.pdf|LTL Assignment]]<br />
** [[Media:Software Synthesis and Verification LTL Assignment-Updated Spec.pdf|Updated Spec for LTL Synthesis Assignment]]<br />
** [[Media:Guidelines for Lab Exercise Report for Synthesis with Acacia.pdf|Guidelines for Assignment]]<br />
** [[Media:Acacia Installation Commands.pdf|Acacia Tool Installation Commands]]<br />
** [[Media:Acacia_Manual.pdf|Acacia Tool Installation Guidelines and Manual for Command Line Options]]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=9120
Software Synthesis and Verification
2020-02-14T08:38:27Z
<p>Leonidas: /* Labs - To be updated from lab 4 on wards */</p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lecturer''': Leonidas Tsiopoulos <br><br />
'''Contact''': leonidas.tsiopoulos ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lecturer''': Maksym Bordin <br><br />
'''Contact''': maksym.bordin ätt ttu.ee, room B404 in the Cybernetics Building <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 10:00, ICT-341 <br><br />
Labs: Tuesdays 12:00, ICT-341 - Evelin Halling<br />
<br />
<br />
'''New!'''<br><br />
'''Exams: (To Be Updated) '''<br />
* ... <br><br />
** Exam is for those who have not passed any of the tests or want to improve their final mark<br />
<!--* ... '''<br />
<br />
--><br />
<br />
==Lecture plan - To be updated for Module II and III==<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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis with Acacia part III - Lecture 14.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:Software Synthesis - Lecture V - Recap.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<br />
* Retake of Test 2, 2nd task: ('''21.05.2019 at 12.00 (New!)''')<br />
** [[Media:Test_2_2019_lahendus.pdf|Eample_Solution]]: ('''Example solution of Task2 (NEW!)''')<br />
<br />
==Labs - To be updated from lab 4 onwards==<br />
* Exercise Environment for Module II:<br />
** Download and install the environment: [[Media:HoareLogic.tar| Hoare Logic environment]]<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 13:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
* Lab 14:<br />
** [[Media:ITI8531_LTL_exercises.pdf|Exercises]]<br />
** [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL tool]<br />
** [http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA]<br />
* Lab 15<br />
** [[Media:ITI8531_LTL_assignments.pdf|LTL Assignment]]<br />
** [[Media:Software Synthesis and Verification LTL Assignment-Updated Spec.pdf|Updated Spec for LTL Synthesis Assignment]]<br />
** [[Media:Guidelines for Lab Exercise Report for Synthesis with Acacia.pdf|Guidelines for Assignment]]<br />
** [[Media:Acacia Installation Commands.pdf|Acacia Tool Installation Commands]]<br />
** [[Media:Acacia_Manual.pdf|Acacia Tool Installation Guidelines and Manual for Command Line Options]]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:HoareLogic.tar&diff=9119
Fail:HoareLogic.tar
2020-02-14T08:36:59Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=9118
Software Synthesis and Verification
2020-02-14T08:36:32Z
<p>Leonidas: /* Labs */</p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lecturer''': Leonidas Tsiopoulos <br><br />
'''Contact''': leonidas.tsiopoulos ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lecturer''': Maksym Bordin <br><br />
'''Contact''': maksym.bordin ätt ttu.ee, room B404 in the Cybernetics Building <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 10:00, ICT-341 <br><br />
Labs: Tuesdays 12:00, ICT-341 - Evelin Halling<br />
<br />
<br />
'''New!'''<br><br />
'''Exams: (To Be Updated) '''<br />
* ... <br><br />
** Exam is for those who have not passed any of the tests or want to improve their final mark<br />
<!--* ... '''<br />
<br />
--><br />
<br />
==Lecture plan - To be updated for Module II and III==<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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis with Acacia part III - Lecture 14.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:Software Synthesis - Lecture V - Recap.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<br />
* Retake of Test 2, 2nd task: ('''21.05.2019 at 12.00 (New!)''')<br />
** [[Media:Test_2_2019_lahendus.pdf|Eample_Solution]]: ('''Example solution of Task2 (NEW!)''')<br />
<br />
==Labs - To be updated from lab 4 on wards==<br />
* Exercise Environment for Module II:<br />
** Download and install the environment: [[Media:HoareLogic.tar| Hoare Logic environment]]<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 13:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
* Lab 14:<br />
** [[Media:ITI8531_LTL_exercises.pdf|Exercises]]<br />
** [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL tool]<br />
** [http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA]<br />
* Lab 15<br />
** [[Media:ITI8531_LTL_assignments.pdf|LTL Assignment]]<br />
** [[Media:Software Synthesis and Verification LTL Assignment-Updated Spec.pdf|Updated Spec for LTL Synthesis Assignment]]<br />
** [[Media:Guidelines for Lab Exercise Report for Synthesis with Acacia.pdf|Guidelines for Assignment]]<br />
** [[Media:Acacia Installation Commands.pdf|Acacia Tool Installation Commands]]<br />
** [[Media:Acacia_Manual.pdf|Acacia Tool Installation Guidelines and Manual for Command Line Options]]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=9117
Software Synthesis and Verification
2020-02-14T08:28:07Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lecturer''': Leonidas Tsiopoulos <br><br />
'''Contact''': leonidas.tsiopoulos ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lecturer''': Maksym Bordin <br><br />
'''Contact''': maksym.bordin ätt ttu.ee, room B404 in the Cybernetics Building <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 10:00, ICT-341 <br><br />
Labs: Tuesdays 12:00, ICT-341 - Evelin Halling<br />
<br />
<br />
'''New!'''<br><br />
'''Exams: (To Be Updated) '''<br />
* ... <br><br />
** Exam is for those who have not passed any of the tests or want to improve their final mark<br />
<!--* ... '''<br />
<br />
--><br />
<br />
==Lecture plan - To be updated for Module II and III==<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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis with Acacia part III - Lecture 14.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:Software Synthesis - Lecture V - Recap.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<br />
* Retake of Test 2, 2nd task: ('''21.05.2019 at 12.00 (New!)''')<br />
** [[Media:Test_2_2019_lahendus.pdf|Eample_Solution]]: ('''Example solution of Task2 (NEW!)''')<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 13:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
* Lab 14:<br />
** [[Media:ITI8531_LTL_exercises.pdf|Exercises]]<br />
** [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL tool]<br />
** [http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA]<br />
* Lab 15<br />
** [[Media:ITI8531_LTL_assignments.pdf|LTL Assignment]]<br />
** [[Media:Software Synthesis and Verification LTL Assignment-Updated Spec.pdf|Updated Spec for LTL Synthesis Assignment]]<br />
** [[Media:Guidelines for Lab Exercise Report for Synthesis with Acacia.pdf|Guidelines for Assignment]]<br />
** [[Media:Acacia Installation Commands.pdf|Acacia Tool Installation Commands]]<br />
** [[Media:Acacia_Manual.pdf|Acacia Tool Installation Guidelines and Manual for Command Line Options]]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=ITI8610&diff=8975
ITI8610
2019-12-09T12:19:20Z
<p>Leonidas: /* Module II: : Assured Software Analytics */</p>
<hr />
<div>'''Course code''': ITI8610 <br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
'''Co-lecturer''': Leonidas Tsiopoulos <br><br />
'''Co-lecturer''': Aleksandr Lenin <br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Thursdays 16:00, ICT-A2 '''NEW!'''<br><br />
Labs: Thursdays 17.45, ICT-A2 <br><br />
* Lab supervisors:<br />
** Aleksandr Lenin (aleksandr.lenin ätt ttu.ee) - Module I<br />
** Jüri Vain (juri.vain ätt ttu.ee), Leonidas Tsiopoulos (letsio ätt ttu.ee) - Module II<br />
<br />
==News 2019==<br />
<br><br />
Deadline for submitting lab assignments of Module II -- TBA<br />
<p><br />
Please fill in [https://doodle.com/poll/3g7333mkn59wp6fe this] Doodle poll and indicate your availability for Module I: Security Assurance lecture and practice slots. Please note that everyone is free to make more than a single choice, you can mark as many slots as you see fit, as well as that every person has 3 options: yes, no, ifneedbe, where yes means this time slot is free for you and you are available at this time, no means you are absolutely unavailable, and ifneedbe means this time slot is unconvenient for you, but if necessary you will be able to make it.<br />
<br />
==Lecture plan==<br />
# [[Media:ITI_8610_lecture_1.pdf|Lecture 1]]: Introduction to software assurance<br />
<br />
<br />
====Module I: Assurance processes, risk management & security assurance====<br />
# [[Media:ITI8610-2019-Risk.pdf|Risks - definitions, terminology, risk taxonomies]]<br />
# [[Media:Risk-Taxonomy-FAIR.pdf|FAIR Risk Taxonomy]]<br />
# [[Media:ITI8610-Riskmanagement.pdf|Risk Management]]<br />
# [[Media:ITI8610-2019-FAIR_Template.zip|Qualitative Risk Analysis Template]]<br />
# [[Media:ITB8811-2019-Probability.pdf|Theory of Probability]]<br />
# [[Media:ITI8610-2019-Reliability.pdf|Reliability and Availability]]<br />
# [[Media:ITI8610-2019-Security_Modeling.pdf|Security Modeling. Quantitative Risk Management]]<br />
<br />
====Module II: : Assured Software Analytics ====<br />
* [[Media:Module_III_Lecture_1.pdf|Module II Lecture 1]]: Design by Contract<br />
* [[Media:Module III 2nd lecture JML Specification Cases.pdf|Module II Lecture 2]]: Specification cases<br />
* [[Media:e.pdf|Module II Lecture 3]]: Multi-view contracts of cyber-physical systems<br />
* [[Media:Module III 4th lecture.pdf|Module II Lecture 4]]: JML contracts for OOP methods<br />
* [[Media:OpenJML - Solvers - 15_11_2018.pdf|Module II Lecture 5]]: OpenJML and SMT Solvers<br />
* [[Media:WorstPracticesInSWDevelopment.pdf|Module II Lecture 6]] (Guest lecture): M. Markvardt (ASA Quality) "Worst Practices in Software Quality a.k.a How to Deal with Risks"<br />
* Lecture 7 (Guest lecture): Dr. Mohammad Al-Taye (Philadelphia Univ., Jordan) "QA by testing"<br />
* Lecture 8: Safety analysis techniques (28.11.2019)<br />
* [[Media:Automotive audio amplifiers.pdf|Module II Lecture 9]] (Guest lecture): R. Kadastik (Adacore) "Automotive audio amplifiers" (5.12.2019)<br />
<br />
==Practice Assignments ==<br />
Possible topics for course project (same topic can be chosen by several teams) <br />
* Smart parking slot /Nutikas parkla<br />
* Moon habitad IGLUNA safety system / Kuuelamu IGLUNA ohutuse tagamise süsteem<br />
* Moon habitad IGLUNA security system / Kuuelamu IGLUNA turbesüsteem<br />
* Railway crossing control / Raudtee ülesõidukoha juhtimine<br />
* Nutikas autode paigutaja praamidele<br />
* Automaatne haigla ravimite annustamise ja kohaletoimetamise süsteem<br />
* Smart home air quality control <br />
* Automaatse tunnustamisega trahvisüsteem<br />
* Automaatne videosalvestussüsteem<br />
* TESLA (auto) juhtimisüsteem <br />
* Bolt tõukerataste rentimissüsteem<br />
* Biometric locking systems (ukse- ja relvalukud).<br />
<br />
==Project Teams==<br />
* Team 1: Allan Paalo, Siim Suviste, Oliver Tooming "TESLA self-driving car"<br />
* Team 2: Krõõt Grete Mänd, Ilja Samoilov "Smart home air quality control"<br />
* Team 3: Veronika Zamakhova, Sergei Zarembo, Dmitri Golovatš "Bolt tõukerataste rentimissüsteem"<br />
* Team 4: Magnus Teekivi, Ly Tempel, Mirjam Pajumägi "Railway crossing control / Raudtee ülesõidukoha juhtimine"<br />
* Team 5: Kristjan-Martin Kirjanen, Kaarel Värk, Andreas Nagel " Biometric locking systems"<br />
* Team 6: Rasmus Tomsen, Henry Härm "Smart video recording system / Automaatne videosalvestuse süsteem"<br />
* Team 7: Johanna Kammiste, Igor Podgainõi "Smart parking slot / Nutikas parkla I"<br />
* Team 8: Kristjan Vool, Regina Helena Lõpp-Elmeste "Smart parking slot / Nutikas parkla II"<br />
<br />
<br />
====Module I: Security Assurance ====<br />
Assignment 1: Perform a qualitative Risk Analysis of your case study using FAIR (Factor Analysis of Information Security Risk) framework and submit a report in pdf format.<br /><br />
Assignment 2: Model one threat in the form of an ADT (Attack-Defense Tree) using the ADTool software http://satoss.uni.lu/members/piotr/adtool/ , export your model in XML format (File->export) and submit the generated XML file.<br /><br />
<br />
====Module II ====<br />
* [[Media:Project_assignment.pdf|Lab instruction]]: Lab assignment plan<br />
* [[Media:OpenJML installation instructions.pdf|OpenJML Installation]]: OpenJML Installation Instructions<br />
NB!<br />
To report completed lab assignments go to web page https://ained.ttu.ee<br />
<br />
and register as user with uniID of TUT<br />
* Some reporting examples from earlier years<br />
** [[Media:Climate_control.pdf| Smart home climate control]]: Project report<br />
** [[Media:Energy_control.pdf| Smart house energy management]]: Project report<br />
<br />
== Grading ==<br />
<br />
Each of the two modules is graded independently on the scale 0-100 points. A student must receive a positive grade in every module. Therefore, a student may obtain max 200 points for the entire course. 51%, or 101 points is the absolute minimum required to pass the course. The standard TalTech grading rules are applied to calculate the student's final grade.<br />
<br />
==Resources==<br />
<br />
https://ained.ttu.ee -- õppekeskkonas olevad materjalid<br /><br />
Gary McGraw "Software Security. Building Security In"<br /></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:Automotive_audio_amplifiers.pdf&diff=8974
Fail:Automotive audio amplifiers.pdf
2019-12-09T12:17:14Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=ITI8610&diff=8973
ITI8610
2019-12-09T12:16:43Z
<p>Leonidas: /* Module II: : Assured Software Analytics */</p>
<hr />
<div>'''Course code''': ITI8610 <br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
'''Co-lecturer''': Leonidas Tsiopoulos <br><br />
'''Co-lecturer''': Aleksandr Lenin <br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Thursdays 16:00, ICT-A2 '''NEW!'''<br><br />
Labs: Thursdays 17.45, ICT-A2 <br><br />
* Lab supervisors:<br />
** Aleksandr Lenin (aleksandr.lenin ätt ttu.ee) - Module I<br />
** Jüri Vain (juri.vain ätt ttu.ee), Leonidas Tsiopoulos (letsio ätt ttu.ee) - Module II<br />
<br />
==News 2019==<br />
<br><br />
Deadline for submitting lab assignments of Module II -- TBA<br />
<p><br />
Please fill in [https://doodle.com/poll/3g7333mkn59wp6fe this] Doodle poll and indicate your availability for Module I: Security Assurance lecture and practice slots. Please note that everyone is free to make more than a single choice, you can mark as many slots as you see fit, as well as that every person has 3 options: yes, no, ifneedbe, where yes means this time slot is free for you and you are available at this time, no means you are absolutely unavailable, and ifneedbe means this time slot is unconvenient for you, but if necessary you will be able to make it.<br />
<br />
==Lecture plan==<br />
# [[Media:ITI_8610_lecture_1.pdf|Lecture 1]]: Introduction to software assurance<br />
<br />
<br />
====Module I: Assurance processes, risk management & security assurance====<br />
# [[Media:ITI8610-2019-Risk.pdf|Risks - definitions, terminology, risk taxonomies]]<br />
# [[Media:Risk-Taxonomy-FAIR.pdf|FAIR Risk Taxonomy]]<br />
# [[Media:ITI8610-Riskmanagement.pdf|Risk Management]]<br />
# [[Media:ITI8610-2019-FAIR_Template.zip|Qualitative Risk Analysis Template]]<br />
# [[Media:ITB8811-2019-Probability.pdf|Theory of Probability]]<br />
# [[Media:ITI8610-2019-Reliability.pdf|Reliability and Availability]]<br />
# [[Media:ITI8610-2019-Security_Modeling.pdf|Security Modeling. Quantitative Risk Management]]<br />
<br />
====Module II: : Assured Software Analytics ====<br />
* [[Media:Module_III_Lecture_1.pdf|Module II Lecture 1]]: Design by Contract<br />
* [[Media:Module III 2nd lecture JML Specification Cases.pdf|Module II Lecture 2]]: Specification cases<br />
* [[Media:e.pdf|Module II Lecture 3]]: Multi-view contracts of cyber-physical systems<br />
* [[Media:Module III 4th lecture.pdf|Module II Lecture 4]]: JML contracts for OOP methods<br />
* [[Media:OpenJML - Solvers - 15_11_2018.pdf|Module II Lecture 5]]: OpenJML and SMT Solvers<br />
* [[Media:WorstPracticesInSWDevelopment.pdf|Module II Lecture 6]] (Guest lecture): M. Markvardt (ASA Quality) "Worst Practices in Software Quality a.k.a How to Deal with Risks"<br />
* Lecture 7 (Guest lecture): Dr. Mohammad Al-Taye (Philadelphia Univ., Jordan) "QA by testing"<br />
* Lecture 8: Safety analysis techniques (28.11.2019)<br />
* [[Media:Automotive audio amplifiers.pdf|Module II Lecture 9]] (Guest lecture): R. Kadastik (Adacore) "IoT tarkava töökindluse köögipoolest" (5.12.2019)<br />
<br />
==Practice Assignments ==<br />
Possible topics for course project (same topic can be chosen by several teams) <br />
* Smart parking slot /Nutikas parkla<br />
* Moon habitad IGLUNA safety system / Kuuelamu IGLUNA ohutuse tagamise süsteem<br />
* Moon habitad IGLUNA security system / Kuuelamu IGLUNA turbesüsteem<br />
* Railway crossing control / Raudtee ülesõidukoha juhtimine<br />
* Nutikas autode paigutaja praamidele<br />
* Automaatne haigla ravimite annustamise ja kohaletoimetamise süsteem<br />
* Smart home air quality control <br />
* Automaatse tunnustamisega trahvisüsteem<br />
* Automaatne videosalvestussüsteem<br />
* TESLA (auto) juhtimisüsteem <br />
* Bolt tõukerataste rentimissüsteem<br />
* Biometric locking systems (ukse- ja relvalukud).<br />
<br />
==Project Teams==<br />
* Team 1: Allan Paalo, Siim Suviste, Oliver Tooming "TESLA self-driving car"<br />
* Team 2: Krõõt Grete Mänd, Ilja Samoilov "Smart home air quality control"<br />
* Team 3: Veronika Zamakhova, Sergei Zarembo, Dmitri Golovatš "Bolt tõukerataste rentimissüsteem"<br />
* Team 4: Magnus Teekivi, Ly Tempel, Mirjam Pajumägi "Railway crossing control / Raudtee ülesõidukoha juhtimine"<br />
* Team 5: Kristjan-Martin Kirjanen, Kaarel Värk, Andreas Nagel " Biometric locking systems"<br />
* Team 6: Rasmus Tomsen, Henry Härm "Smart video recording system / Automaatne videosalvestuse süsteem"<br />
* Team 7: Johanna Kammiste, Igor Podgainõi "Smart parking slot / Nutikas parkla I"<br />
* Team 8: Kristjan Vool, Regina Helena Lõpp-Elmeste "Smart parking slot / Nutikas parkla II"<br />
<br />
<br />
====Module I: Security Assurance ====<br />
Assignment 1: Perform a qualitative Risk Analysis of your case study using FAIR (Factor Analysis of Information Security Risk) framework and submit a report in pdf format.<br /><br />
Assignment 2: Model one threat in the form of an ADT (Attack-Defense Tree) using the ADTool software http://satoss.uni.lu/members/piotr/adtool/ , export your model in XML format (File->export) and submit the generated XML file.<br /><br />
<br />
====Module II ====<br />
* [[Media:Project_assignment.pdf|Lab instruction]]: Lab assignment plan<br />
* [[Media:OpenJML installation instructions.pdf|OpenJML Installation]]: OpenJML Installation Instructions<br />
NB!<br />
To report completed lab assignments go to web page https://ained.ttu.ee<br />
<br />
and register as user with uniID of TUT<br />
* Some reporting examples from earlier years<br />
** [[Media:Climate_control.pdf| Smart home climate control]]: Project report<br />
** [[Media:Energy_control.pdf| Smart house energy management]]: Project report<br />
<br />
== Grading ==<br />
<br />
Each of the two modules is graded independently on the scale 0-100 points. A student must receive a positive grade in every module. Therefore, a student may obtain max 200 points for the entire course. 51%, or 101 points is the absolute minimum required to pass the course. The standard TalTech grading rules are applied to calculate the student's final grade.<br />
<br />
==Resources==<br />
<br />
https://ained.ttu.ee -- õppekeskkonas olevad materjalid<br /><br />
Gary McGraw "Software Security. Building Security In"<br /></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:WorstPracticesInSWDevelopment.pdf&diff=8919
Fail:WorstPracticesInSWDevelopment.pdf
2019-11-18T16:15:40Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=ITI8610&diff=8918
ITI8610
2019-11-18T16:12:08Z
<p>Leonidas: /* Module II: : Assured Software Analytics */</p>
<hr />
<div>'''Course code''': ITI8610 <br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
'''Co-lecturer''': Leonidas Tsiopoulos <br><br />
'''Co-lecturer''': Aleksandr Lenin <br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Thursdays 16:00, ICT-A2 '''NEW!'''<br><br />
Labs: Thursdays 17.45, ICT-A2 <br><br />
* Lab supervisors:<br />
** Aleksandr Lenin (aleksandr.lenin ätt ttu.ee) - Module I<br />
** Jüri Vain (juri.vain ätt ttu.ee), Leonidas Tsiopoulos (letsio ätt ttu.ee) - Module II<br />
<br />
==News 2019==<br />
<br><br />
Deadline for submitting lab assignments of Module II -- TBA<br />
<p><br />
Please fill in [https://doodle.com/poll/3g7333mkn59wp6fe this] Doodle poll and indicate your availability for Module I: Security Assurance lecture and practice slots. Please note that everyone is free to make more than a single choice, you can mark as many slots as you see fit, as well as that every person has 3 options: yes, no, ifneedbe, where yes means this time slot is free for you and you are available at this time, no means you are absolutely unavailable, and ifneedbe means this time slot is unconvenient for you, but if necessary you will be able to make it.<br />
<br />
==Lecture plan==<br />
# [[Media:ITI_8610_lecture_1.pdf|Lecture 1]]: Introduction to software assurance<br />
<br />
<br />
====Module I: Assurance processes, risk management & security assurance====<br />
# [[Media:ITI8610-2019-Risk.pdf|Risks - definitions, terminology, risk taxonomies]]<br />
# [[Media:Risk-Taxonomy-FAIR.pdf|FAIR Risk Taxonomy]]<br />
# [[Media:ITI8610-Riskmanagement.pdf|Risk Management]]<br />
# [[Media:ITI8610-2019-FAIR_Template.zip|Qualitative Risk Analysis Template]]<br />
# [[Media:ITB8811-2019-Probability.pdf|Theory of Probability]]<br />
# [[Media:ITI8610-2019-Reliability.pdf|Reliability and Availability]]<br />
# [[Media:ITI8610-2019-Security_Modeling.pdf|Security Modeling. Quantitative Risk Management]]<br />
<br />
====Module II: : Assured Software Analytics ====<br />
* [[Media:Module_III_Lecture_1.pdf|Module II Lecture 1]]: Design by Contract<br />
* [[Media:Module III 2nd lecture JML Specification Cases.pdf|Module II Lecture 2]]: Specification cases<br />
* [[Media:e.pdf|Module II Lecture 3]]: Multi-view contracts of cyber-physical systems<br />
* [[Media:Module III 4th lecture.pdf|Module II Lecture 4]]: JML contracts for OOP methods<br />
* [[Media:OpenJML - Solvers - 15_11_2018.pdf|Module II Lecture 5]]: OpenJML and SMT Solvers<br />
* [[Media:WorstPracticesInSWDevelopment.pdf|Module II Lecture 6]]: Worst Practices in Software Quality a.k.a How to Deal with Risks<br />
<br />
==Practice Assignments ==<br />
Possible topics for course project (same topic can be chosen by several teams) <br />
* Smart parking slot /Nutikas parkla<br />
* Moon habitad IGLUNA safety system / Kuuelamu IGLUNA ohutuse tagamise süsteem<br />
* Moon habitad IGLUNA security system / Kuuelamu IGLUNA turbesüsteem<br />
* Railway crossing control / Raudtee ülesõidukoha juhtimine<br />
* Nutikas autode paigutaja praamidele<br />
* Automaatne haigla ravimite annustamise ja kohaletoimetamise süsteem<br />
* Smart home air quality control <br />
* Automaatse tunnustamisega trahvisüsteem<br />
* Automaatne videosalvestussüsteem<br />
* TESLA (auto) juhtimisüsteem <br />
* Bolt tõukerataste rentimissüsteem<br />
* Biometric locking systems (ukse- ja relvalukud).<br />
<br />
==Project Teams==<br />
* Team 1: Allan Paalo, Siim Suviste, Oliver Tooming "TESLA self-driving car"<br />
* Team 2: Krõõt Grete Mänd, Ilja Samoilov "Smart home air quality control"<br />
* Team 3: Veronika Zamakhova, Sergei Zarembo, Dmitri Golovatš "Bolt tõukerataste rentimissüsteem"<br />
* Team 4: Magnus Teekivi, Ly Tempel, Mirjam Pajumägi "Railway crossing control / Raudtee ülesõidukoha juhtimine"<br />
* Team 5: Kristjan-Martin Kirjanen, Kaarel Värk, Andreas Nagel " Biometric locking systems"<br />
* Team 6: Rasmus Tomsen, Henry Härm "Smart video recording system / Automaatne videosalvestuse süsteem"<br />
* Team 7: Johanna Kammiste, Igor Podgainõi "Smart parking slot / Nutikas parkla I"<br />
* Team 8: Kristjan Vool, Regina Helena Lõpp-Elmeste "Smart parking slot / Nutikas parkla II"<br />
<br />
<br />
====Module I: Security Assurance ====<br />
Assignment 1: Perform a qualitative Risk Analysis of your case study using FAIR (Factor Analysis of Information Security Risk) framework and submit a report in pdf format.<br /><br />
Assignment 2: Model one threat in the form of an ADT (Attack-Defense Tree) using the ADTool software http://satoss.uni.lu/members/piotr/adtool/ , export your model in XML format (File->export) and submit the generated XML file.<br /><br />
<br />
====Module II ====<br />
* [[Media:Project_assignment.pdf|Lab instruction]]: Lab assignment plan<br />
* [[Media:OpenJML installation instructions.pdf|OpenJML Installation]]: OpenJML Installation Instructions<br />
NB!<br />
To report completed lab assignments go to web page https://ained.ttu.ee<br />
<br />
and register as user with uniID of TUT<br />
* Some reporting examples from earlier years<br />
** [[Media:Climate_control.pdf| Smart home climate control]]: Project report<br />
** [[Media:Energy_control.pdf| Smart house energy management]]: Project report<br />
<br />
== Grading ==<br />
<br />
Each of the two modules is graded independently on the scale 0-100 points. A student must receive a positive grade in every module. Therefore, a student may obtain max 200 points for the entire course. 51%, or 101 points is the absolute minimum required to pass the course. The standard TalTech grading rules are applied to calculate the student's final grade.<br />
<br />
==Resources==<br />
<br />
https://ained.ttu.ee -- õppekeskkonas olevad materjalid<br /><br />
Gary McGraw "Software Security. Building Security In"<br /></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:OpenJML_installation_instructions.pdf&diff=8844
Fail:OpenJML installation instructions.pdf
2019-10-31T12:03:43Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=ITI8610&diff=8843
ITI8610
2019-10-31T12:03:09Z
<p>Leonidas: /* Module II */</p>
<hr />
<div>'''Course code''': ITI8610 <br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
'''Co-lecturer''': Leonidas Tsiopoulos <br><br />
'''Co-lecturer''': Aleksandr Lenin <br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Thursdays 16:00, ICT-A2 '''NEW!'''<br><br />
Labs: Thursdays 17.45, ICT-A2 <br><br />
* Lab supervisors:<br />
** Aleksandr Lenin (aleksandr.lenin ätt ttu.ee) - Module I<br />
** Jüri Vain (juri.vain ätt ttu.ee), Leonidas Tsiopoulos (letsio ätt ttu.ee) - Module II<br />
<br />
==News 2019==<br />
<br><br />
Deadline for submitting lab assignments of Module II -- TBA<br />
<p><br />
Please fill in [https://doodle.com/poll/3g7333mkn59wp6fe this] Doodle poll and indicate your availability for Module I: Security Assurance lecture and practice slots. Please note that everyone is free to make more than a single choice, you can mark as many slots as you see fit, as well as that every person has 3 options: yes, no, ifneedbe, where yes means this time slot is free for you and you are available at this time, no means you are absolutely unavailable, and ifneedbe means this time slot is unconvenient for you, but if necessary you will be able to make it.<br />
<br />
==Lecture plan==<br />
# [[Media:ITI_8610_lecture_1.pdf|Lecture 1]]: Introduction to software assurance<br />
<br />
<br />
====Module I: Assurance processes, risk management & security assurance====<br />
# [[Media:ITI8610-2019-Risk.pdf|Risks - definitions, terminology, risk taxonomies]]<br />
# [[Media:Risk-Taxonomy-FAIR.pdf|FAIR Risk Taxonomy]]<br />
# [[Media:ITI8610-Riskmanagement.pdf|Risk Management]]<br />
# [[Media:ITI8610-2019-FAIR_Template.zip|Qualitative Risk Analysis Template]]<br />
# [[Media:ITB8811-2019-Probability.pdf|Theory of Probability]]<br />
# [[Media:ITI8610-2019-Reliability.pdf|Reliability and Availability]]<br />
# [[Media:ITI8610-2019-Security_Modeling.pdf|Security Modeling. Quantitative Risk Management]]<br />
<br />
====Module II: : Assured Software Analytics ====<br />
* [[Media:Module_III_Lecture_1.pdf|Module II Lecture 1]]: Design by Contract<br />
* [[Media:Module III 2nd lecture JML Specification Cases.pdf|Module II Lecture 2]]: Specification cases<br />
* [[Media:e.pdf|Module II Lecture 3]]: Multi-view contracts of cyber-physical systems<br />
* [[Media:Module III 4th lecture.pdf|Module II Lecture 4]]: JML contracts for OOP methods<br />
* [[Media:OpenJML - Solvers - 15_11_2018.pdf|Module II Lecture 5]]: OpenJML and SMT Solvers<br />
<br />
==Practice Assignments ==<br />
Possible topics for course project (same topic can be chosen by several teams) <br />
* Smart parking slot /Nutikas parkla<br />
* Moon habitad IGLUNA safety system / Kuuelamu IGLUNA ohutuse tagamise süsteem<br />
* Moon habitad IGLUNA security system / Kuuelamu IGLUNA turbesüsteem<br />
* Railway crossing control / Raudtee ülesõidukoha juhtimine<br />
* Nutikas autode paigutaja praamidele<br />
* Automaatne haigla ravimite annustamise ja kohaletoimetamise süsteem<br />
* Smart home air quality control <br />
* Automaatse tunnustamisega trahvisüsteem<br />
* Automaatne videosalvestussüsteem<br />
* TESLA (auto) juhtimisüsteem <br />
* Bolt tõukerataste rentimissüsteem<br />
* Biometric locking systems (ukse- ja relvalukud).<br />
<br />
==Project Teams==<br />
* Team 1: Allan Paalo, Siim Suviste, Oliver Tooming "TESLA self-driving car"<br />
* Team 2: Krõõt Grete Mänd, Ilja Samoilov "Smart home air quality control"<br />
* Team 3: Veronika Zamakhova, Sergei Zarembo, Dmitri Golovatš "Bolt tõukerataste rentimissüsteem"<br />
* Team 4: Magnus Teekivi, Ly Tempel, Mirjam Pajumägi "Railway crossing control / Raudtee ülesõidukoha juhtimine"<br />
* Team 5: Kristjan-Martin Kirjanen, Kaarel Värk, Andreas Nagel " Biometric locking systems"<br />
* Team 6: Rasmus Tomsen, Henry Härm "Smart video recording system / Automaatne videosalvestuse süsteem"<br />
* Team 7: Johanna Kammiste, Igor Podgainõi "Smart parking slot / Nutikas parkla I"<br />
* Team 8: Kristjan Vool, Regina Helena Lõpp-Elmeste "Smart parking slot / Nutikas parkla II"<br />
<br />
<br />
====Module I: Security Assurance ====<br />
Assignment 1: Perform a qualitative Risk Analysis of your case study using FAIR (Factor Analysis of Information Security Risk) framework and submit a report in pdf format.<br /><br />
Assignment 2: Model one threat in the form of an ADT (Attack-Defense Tree) using the ADTool software http://satoss.uni.lu/members/piotr/adtool/ , export your model in XML format (File->export) and submit the generated XML file.<br /><br />
<br />
====Module II ====<br />
* [[Media:Project_assignment.pdf|Lab instruction]]: Lab assignment plan<br />
* [[Media:OpenJML installation instructions.pdf|OpenJML Installation]]: OpenJML Installation Instructions<br />
NB!<br />
To report completed lab assignments go to web page https://ained.ttu.ee<br />
<br />
and register as user with uniID of TUT<br />
* Some reporting examples from earlier years<br />
** [[Media:Climate_control.pdf| Smart home climate control]]: Project report<br />
** [[Media:Energy_control.pdf| Smart house energy management]]: Project report<br />
<br />
== Grading ==<br />
<br />
Each of the two modules is graded independently on the scale 0-100 points. A student must receive a positive grade in every module. Therefore, a student may obtain max 200 points for the entire course. 51%, or 101 points is the absolute minimum required to pass the course. The standard TalTech grading rules are applied to calculate the student's final grade.<br />
<br />
==Resources==<br />
<br />
https://ained.ttu.ee -- õppekeskkonas olevad materjalid<br /><br />
Gary McGraw "Software Security. Building Security In"<br /></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:Software_Synthesis_-_Lecture_V_-_Recap.pdf&diff=8387
Fail:Software Synthesis - Lecture V - Recap.pdf
2019-05-14T14:44:05Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=8386
Software Synthesis and Verification
2019-05-14T14:43:30Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lecturer''': Leonidas Tsiopoulos <br><br />
'''Contact''': leonidas.tsiopoulos ätt ttu.ee, ICT-424 <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 12:00, ICT-A1 <br><br />
Labs: Thursdays 10:00, ICT-A1 - Evelin Halling<br />
<!--<br />
'''New!'''<br><br />
'''Exams: '''<br />
* Thursday May 24, 10:00, room ICT-A1 <br><br />
* Thursday May 31, 10:00, room ICT-A1'''<br />
--><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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis with Acacia part III - Lecture 14.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:Software Synthesis - Lecture V - Recap.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 13:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
* Lab 14:<br />
** [[Media:ITI8531_LTL_exercises.pdf|Exercises]]<br />
** [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL tool]<br />
** [http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA]<br />
* Lab 15<br />
** [[Media:ITI8531_LTL_assignments.pdf|LTL Assignment]]<br />
** [[Media:Software Synthesis and Verification LTL Assignment-Updated Spec.pdf|Updated Spec for LTL Synthesis Assignment]]<br />
** [[Media:Guidelines for Lab Exercise Report for Synthesis with Acacia.pdf|Guidelines for Assignment]]<br />
** [[Media:Acacia Installation Commands.pdf|Acacia Tool Installation Commands]]<br />
** [[Media:Acacia_Manual.pdf|Acacia Tool Installation Guidelines and Manual for Command Line Options]]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:Software_Synthesis_and_Verification_LTL_Assignment-Updated_Spec.pdf&diff=8385
Fail:Software Synthesis and Verification LTL Assignment-Updated Spec.pdf
2019-05-14T07:36:49Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=8384
Software Synthesis and Verification
2019-05-14T07:36:00Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lecturer''': Leonidas Tsiopoulos <br><br />
'''Contact''': leonidas.tsiopoulos ätt ttu.ee, ICT-424 <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 12:00, ICT-A1 <br><br />
Labs: Thursdays 10:00, ICT-A1 - Evelin Halling<br />
<!--<br />
'''New!'''<br><br />
'''Exams: '''<br />
* Thursday May 24, 10:00, room ICT-A1 <br><br />
* Thursday May 31, 10:00, room ICT-A1'''<br />
--><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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis with Acacia part III - Lecture 14.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 13:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
* Lab 14:<br />
** [[Media:ITI8531_LTL_exercises.pdf|Exercises]]<br />
** [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL tool]<br />
** [http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA]<br />
* Lab 15<br />
** [[Media:ITI8531_LTL_assignments.pdf|LTL Assignment]]<br />
** [[Media:Software Synthesis and Verification LTL Assignment-Updated Spec.pdf|Updated Spec for LTL Synthesis Assignment]]<br />
** [[Media:Guidelines for Lab Exercise Report for Synthesis with Acacia.pdf|Guidelines for Assignment]]<br />
** [[Media:Acacia Installation Commands.pdf|Acacia Tool Installation Commands]]<br />
** [[Media:Acacia_Manual.pdf|Acacia Tool Installation Guidelines and Manual for Command Line Options]]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:Acacia_Manual.pdf&diff=8369
Fail:Acacia Manual.pdf
2019-05-10T07:10:12Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=8368
Software Synthesis and Verification
2019-05-10T07:09:08Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 12:00, ICT-A1 <br><br />
Labs: Thursdays 10:00, ICT-A1 - Evelin Halling<br />
<!--<br />
'''New!'''<br><br />
'''Exams: '''<br />
* Thursday May 24, 10:00, room ICT-A1 <br><br />
* Thursday May 31, 10:00, room ICT-A1'''<br />
--><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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis with Acacia part III - Lecture 14.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 13:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
* Lab 14:<br />
** [[Media:ITI8531_LTL_exercises.pdf|Exercises]]<br />
** [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL tool]<br />
** [http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA]<br />
* Lab 15<br />
** [[Media:ITI8531_LTL_assignments.pdf|LTL Assignment]]<br />
** [[Media:Guidelines for Lab Exercise Report for Synthesis with Acacia.pdf|Guidelines for Assignment]]<br />
** [[Media:Acacia Installation Commands.pdf|Acacia Tool Installation Commands]]<br />
** [[Media:Acacia_Manual.pdf|Acacia Tool Installation Guidelines and Manual for Command Line Options]]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:Acacia_Installation_Commands.pdf&diff=8362
Fail:Acacia Installation Commands.pdf
2019-05-09T09:11:31Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=8361
Software Synthesis and Verification
2019-05-09T09:11:00Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 12:00, ICT-A1 <br><br />
Labs: Thursdays 10:00, ICT-A1 - Evelin Halling<br />
<!--<br />
'''New!'''<br><br />
'''Exams: '''<br />
* Thursday May 24, 10:00, room ICT-A1 <br><br />
* Thursday May 31, 10:00, room ICT-A1'''<br />
--><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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis with Acacia part III - Lecture 14.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 13:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
* Lab 14:<br />
** [[Media:ITI8531_LTL_exercises.pdf|Exercises]]<br />
** [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL tool]<br />
** [http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA]<br />
* Lab 15<br />
** [[Media:ITI8531_LTL_assignments.pdf|LTL Assignment]]<br />
** [[Media:Guidelines for Lab Exercise Report for Synthesis with Acacia.pdf|Guidelines for Assignment]]<br />
** [[Media:Acacia Installation Commands.pdf|Acacia Tool Installation Commands]]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:Guidelines_for_Lab_Exercise_Report_for_Synthesis_with_Acacia.pdf&diff=8360
Fail:Guidelines for Lab Exercise Report for Synthesis with Acacia.pdf
2019-05-09T09:04:05Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=8359
Software Synthesis and Verification
2019-05-09T09:03:35Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 12:00, ICT-A1 <br><br />
Labs: Thursdays 10:00, ICT-A1 - Evelin Halling<br />
<!--<br />
'''New!'''<br><br />
'''Exams: '''<br />
* Thursday May 24, 10:00, room ICT-A1 <br><br />
* Thursday May 31, 10:00, room ICT-A1'''<br />
--><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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis with Acacia part III - Lecture 14.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 13:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
* Lab 14:<br />
** [[Media:ITI8531_LTL_exercises.pdf|Exercises]]<br />
** [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL tool]<br />
** [http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA]<br />
* Lab 15<br />
** [[Media:ITI8531_LTL_assignments.pdf|LTL Assignment]]<br />
** [[Media:Guidelines for Lab Exercise Report for Synthesis with Acacia.pdf|Guidelines for Assignment]]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:Software_Synthesis_-_LTL_Synthesis_with_Acacia_part_III_-_Lecture_14.pdf&diff=8348
Fail:Software Synthesis - LTL Synthesis with Acacia part III - Lecture 14.pdf
2019-05-07T14:59:34Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=8347
Software Synthesis and Verification
2019-05-07T14:59:09Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 12:00, ICT-A1 <br><br />
Labs: Thursdays 10:00, ICT-A1 - Evelin Halling<br />
<!--<br />
'''New!'''<br><br />
'''Exams: '''<br />
* Thursday May 24, 10:00, room ICT-A1 <br><br />
* Thursday May 31, 10:00, room ICT-A1'''<br />
--><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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis with Acacia part III - Lecture 14.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 13:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
* Lab 14:<br />
** [[Media:ITI8531_LTL_exercises.pdf|Exercises]]<br />
** [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL tool]<br />
** [http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA]<br />
* Lab 15<br />
** [[Media:ITI8531_LTL_assignments.pdf|LTL Assignment]]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=8318
Software Synthesis and Verification
2019-04-30T13:07:33Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 12:00, ICT-A1 <br><br />
Labs: Thursdays 10:00, ICT-A1 - Evelin Halling<br />
<!--<br />
'''New!'''<br><br />
'''Exams: '''<br />
* Thursday May 24, 10:00, room ICT-A1 <br><br />
* Thursday May 31, 10:00, room ICT-A1'''<br />
--><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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Media:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 13:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
* Lab 14:<br />
** [[Media:ITI8531_LTL_exercises.pdf|Exercises]]<br />
** [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL tool]<br />
** [http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:Software_Synthesis_-_LTL_Synthesis_and_Acacia_II_-_Lecture_13.pdf&diff=8317
Fail:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf
2019-04-30T12:57:36Z
<p>Leonidas: Leonidas laadis üles faili &quot;Pilt:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf&quot; uue versiooni</p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:Software_Synthesis_-_LTL_Synthesis_and_Acacia_II_-_Lecture_13.pdf&diff=8316
Fail:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf
2019-04-30T12:36:11Z
<p>Leonidas: Leonidas laadis üles faili &quot;Pilt:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf&quot; uue versiooni</p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:Software_Synthesis_-_LTL_Synthesis_and_Acacia_II_-_Lecture_13.pdf&diff=8315
Fail:Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf
2019-04-30T12:34:33Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=8314
Software Synthesis and Verification
2019-04-30T12:30:49Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 12:00, ICT-A1 <br><br />
Labs: Thursdays 10:00, ICT-A1 - Evelin Halling<br />
<!--<br />
'''New!'''<br><br />
'''Exams: '''<br />
* Thursday May 24, 10:00, room ICT-A1 <br><br />
* Thursday May 31, 10:00, room ICT-A1'''<br />
--><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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Software Synthesis - LTL Synthesis and Acacia II - Lecture 13.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 13:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
* Lab 14:<br />
** [[Media:ITI8531_LTL_exercises.pdf|Exercises]]<br />
** [http://goal.im.ntu.edu.tw/wiki/doku.php GOAL tool]<br />
** [http://www.lsv.fr/~gastin/ltl2ba/ LTL2BA]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=8294
Software Synthesis and Verification
2019-04-23T13:25:42Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 12:00, ICT-A1 <br><br />
Labs: Thursdays 10:00, ICT-A1 - Evelin Halling<br />
<!--<br />
'''New!'''<br><br />
'''Exams: '''<br />
* Thursday May 24, 10:00, room ICT-A1 <br><br />
* Thursday May 31, 10:00, room ICT-A1'''<br />
--><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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Software synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Software synthesis II (23.04.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 13]]: Software synthesis III (30.04.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 14]]: Software synthesis IV (7.05.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 15]]: Software synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Software synthesis ('''16.05.2019''')<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 12:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:Software_Synthesis_-_Introduction_to_Acacia_-_Lecture_12.pdf&diff=8293
Fail:Software Synthesis - Introduction to Acacia - Lecture 12.pdf
2019-04-23T13:21:54Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=8292
Software Synthesis and Verification
2019-04-23T13:21:20Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 12:00, ICT-A1 <br><br />
Labs: Thursdays 10:00, ICT-A1 - Evelin Halling<br />
<!--<br />
'''New!'''<br><br />
'''Exams: '''<br />
* Thursday May 24, 10:00, room ICT-A1 <br><br />
* Thursday May 31, 10:00, room ICT-A1'''<br />
--><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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Program synthesis I (16.04.2019)<br />
* [[Media:Software Synthesis - Introduction to Acacia - Lecture 12.pdf|Lecture 12]]: Program synthesis II (23.04.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 13]]: Program synthesis III (30.04.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 14]]: Program synthesis IV (7.05.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 15]]: Program synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Program synthesis ('''16.05.2017''')<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<br />
* Lab 12:<br />
** [http://web.iitd.ac.in/~sumeet/slide3.pdf LTL]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:Software_Synthesis_-_Overview_of_Temporal_Synthesis_-_Lecture_11.pdf&diff=8286
Fail:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf
2019-04-16T10:21:17Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Software_Synthesis_and_Verification&diff=8285
Software Synthesis and Verification
2019-04-16T10:20:46Z
<p>Leonidas: </p>
<hr />
<div>'''Course code''': ITI8531 <br><br />
'''Link''': http://courses.cs.ttu.ee/pages/ITI0130<br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
<br />
'''Lab assistant''': <br />
Evelin Halling <br><br />
'''Contact''': evelin.halling ätt ttu.ee, <br><br />
<br />
<br />
<br />
Previous courses: [http://vana.cs.ttu.ee/tiki-index.php?page=ITI0060 2014]<br />
<br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Tuesdays 12:00, ICT-A1 <br><br />
Labs: Thursdays 10:00, ICT-A1 - Evelin Halling<br />
<!--<br />
'''New!'''<br><br />
'''Exams: '''<br />
* Thursday May 24, 10:00, room ICT-A1 <br><br />
* Thursday May 31, 10:00, room ICT-A1'''<br />
--><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: Model checking [[Media:ITI8531_Exercises_1_2016.pdf|Exercises]]: (05.03.2019)<br />
* Test 1: Model checking ('''12.03.2019''')<br />
* [[Media:ITI8531_Lecture_6.1_18_Specifications.pdf|Lecture 6]]: Program specifications (19.03.2019)<br />
* [[Media:ITI8531_Lecture_6.2_18_verification.pdf|Lecture 7]]: Proving partial correctness of programs (19.03.2019)<br />
* [[Media:ITI8531_Lecture_7_18_proving (2).pdf|Lecture 8]]: Proof techniques (1): derived rules, backwards proof, annotations (26.03.2019)<br />
* [[Media:ITI8531_Lecture_8_18_total_correctness.pdf|Lecture 9]]: Proving total correctness of while-programs (26.03.2019)<br />
* [[Media:ITI8531_Lecture_9_2017_parallel_programs.pdf|Lecture 10]]: Verifying nondeterministic and parallel programs (02.04.2019)<br />
* Practicing for Test 2: Deductive verification of non-deterministic and parallel programs (04.04.2019 at lab time)<br />
** [[Media:ITI8531_Genzen_1st_order_calculus.pdf|Genzen 1st order calculus]]: Genzen 1st order sequent calculus (proof rules)<br />
* Test 2: Deductive verification of sequential, non-deterministic and parallel programs ('''09.04.2019,at 12.00''')<br />
* [[Media:Software Synthesis - Overview of Temporal Synthesis - Lecture 11.pdf|Lecture 11]]: Program synthesis I (16.04.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 12]]: Program synthesis II (23.04.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 13]]: Program synthesis III (30.04.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 14]]: Program synthesis IV (7.05.2019)<br />
* [[Media:ITI8531_synthesis2_2017.pdf|Lecture 15]]: Program synthesis (recap) and practicing for test (14.05.2019)<br />
* Test 3: Program synthesis ('''16.05.2017''')<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 I: Reader-Writer (unreliable) communication protocol<br />
** Slides: [[Media:ITI0130_Lab2_2015.pdf|Example and explanation]]<br />
<br />
* Lab 5: Assignment II: 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, page 172]]<br />
<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 />
<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 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 />
--><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'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's lecture notes on Hoare logic [http://www.lsv.ens-cachan.fr/~demri/Gordon14.pdf]</div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=ITI8610&diff=7812
ITI8610
2018-11-29T10:43:11Z
<p>Leonidas: /* Module II: : Assured Software Analytics */</p>
<hr />
<div>'''Course code''': ITI8610 <br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
'''Co-lecturer''': Leonidas Tsiopoulos <br><br />
'''Co-lecturer''': Aleksandr Lenin <br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Wednesdays 10:00, ICT-315 <br><br />
Labs: Wednesdays 12.00 <br><br />
* Lab supervisors:<br />
** Aleksandr Lenin (aleksandr.lenin ätt ttu.ee) - Module I<br />
** Jüri Vain (juri.vain ätt ttu.ee), Leonidas Tsiopoulos (letsio ätt ttu.ee) - Module II<br />
<br />
==News 2018==<br />
<br><br />
Deadline for submitting lab assignments of Module II -- TBA<br />
<br />
==Lecture plan==<br />
* [[Media:ITI_8610_lecture_1.pdf|Lecture 1]]: Introduction to software assurance<br />
====Module I: Assurance processes, risk management & security assurance==== ====<br />
Lecture 1: Security Risk Management<br /><br />
Lecture 2: Security Risk Management (contd.)<br /><br />
Lecture 3: Security Best Practices<br /><br />
Lecture 4: Input Validation<br /><br />
Lecture 5. Web Application Security. Cross-Site Scripting Attacks<br /><br />
<br />
====Module II: : Assured Software Analytics ====<br />
* [[Media:Module_III_Lecture_1.pdf|Module II Lecture 1]]: Design by Contract<br />
* [[Media:Module III 2nd lecture JML Specification Cases.pdf|Module II Lecture 2]]: Specification cases<br />
* [[Media:e.pdf|Module II Lecture 3]]: Multi-view contracts of cyber-physical systems<br />
* [[Media:Module III 4th lecture.pdf|Module II Lecture 4]]: JML contracts for OOP methods<br />
* [[Media:OpenJML - Solvers - 15_11_2018.pdf|Module II Lecture 5]]: OpenJML and SMT Solvers<br />
<br />
==Practice Assignments==<br />
====Module I: Security Assurance ====<br />
Assignment 1: Risk Analysis using the FAIR (Factor Analysis of Information Security Risk) framework<br /><br />
Assignment 2: Vulnerability Identification in Code using Static Analysis Tools<br /><br />
Assignment 3: Architectural Risk Analysis<br /><br />
Assignment 4: Web Application Exploitation<br />
<br />
====Module II ====<br />
* [[Media:HomeAssignmnet_of ModuleII.pdf|Lab instruction]]: Lab assignment plan<br />
NB!<br />
To report completed lab assignments go to web page https://ained.ttu.ee<br />
<br />
and register as user with uniID of TUT<br />
<br />
== Grading ==<br />
<br />
Each of the two modules is graded independently on the scale 0-100 points. A student must receive a positive grade in every module. Therefore, a student may obtain max 200 points for the entire course. 51%, or 101 points is the absolute minimum required to pass the course. The standard TalTech grading rules are applied to calculate the student's final grade.<br />
<br />
==Resources==<br />
<br />
https://ained.ttu.ee -- õppekeskkonas olevad materjalid<br /><br />
Gary McGraw "Software Security. Building Security In"<br /></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=Fail:OpenJML_-_Solvers_-_15_11_2018.pdf&diff=7811
Fail:OpenJML - Solvers - 15 11 2018.pdf
2018-11-29T10:40:35Z
<p>Leonidas: </p>
<hr />
<div></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=ITI8610&diff=7810
ITI8610
2018-11-29T10:39:22Z
<p>Leonidas: /* Module II: : Assured Software Analytics */</p>
<hr />
<div>'''Course code''': ITI8610 <br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
'''Co-lecturer''': Leonidas Tsiopoulos <br><br />
'''Co-lecturer''': Aleksandr Lenin <br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Wednesdays 10:00, ICT-315 <br><br />
Labs: Wednesdays 12.00 <br><br />
* Lab supervisors:<br />
** Aleksandr Lenin (aleksandr.lenin ätt ttu.ee) - Module I<br />
** Jüri Vain (juri.vain ätt ttu.ee), Leonidas Tsiopoulos (letsio ätt ttu.ee) - Module II<br />
<br />
==News 2018==<br />
<br><br />
Deadline for submitting lab assignments of Module II -- TBA<br />
<br />
==Lecture plan==<br />
* [[Media:ITI_8610_lecture_1.pdf|Lecture 1]]: Introduction to software assurance<br />
====Module I: Assurance processes, risk management & security assurance==== ====<br />
Lecture 1: Security Risk Management<br /><br />
Lecture 2: Security Risk Management (contd.)<br /><br />
Lecture 3: Security Best Practices<br /><br />
Lecture 4: Input Validation<br /><br />
Lecture 5. Web Application Security. Cross-Site Scripting Attacks<br /><br />
<br />
====Module II: : Assured Software Analytics ====<br />
* [[Media:Module_III_Lecture_1.pdf|Module II Lecture 1]]: Design by Contract<br />
* [[Media:Module III 2nd lecture JML Specification Cases.pdf|Module II Lecture 2]]: Specification cases<br />
* [[Media:e.pdf|Module II Lecture 3]]: Multi-view contracts of cyber-physical systems<br />
* [[Media:Module III 4th lecture.pdf|Module II Lecture 4]]: JML contracts for OOP methods<br />
* [[Media:OpenJML - Solvers - 15_11_2018.pdf|Module II Lecture 5]]: A Tutorial on OpenJML<br />
<br />
==Practice Assignments==<br />
====Module I: Security Assurance ====<br />
Assignment 1: Risk Analysis using the FAIR (Factor Analysis of Information Security Risk) framework<br /><br />
Assignment 2: Vulnerability Identification in Code using Static Analysis Tools<br /><br />
Assignment 3: Architectural Risk Analysis<br /><br />
Assignment 4: Web Application Exploitation<br />
<br />
====Module II ====<br />
* [[Media:HomeAssignmnet_of ModuleII.pdf|Lab instruction]]: Lab assignment plan<br />
NB!<br />
To report completed lab assignments go to web page https://ained.ttu.ee<br />
<br />
and register as user with uniID of TUT<br />
<br />
== Grading ==<br />
<br />
Each of the two modules is graded independently on the scale 0-100 points. A student must receive a positive grade in every module. Therefore, a student may obtain max 200 points for the entire course. 51%, or 101 points is the absolute minimum required to pass the course. The standard TalTech grading rules are applied to calculate the student's final grade.<br />
<br />
==Resources==<br />
<br />
https://ained.ttu.ee -- õppekeskkonas olevad materjalid<br /><br />
Gary McGraw "Software Security. Building Security In"<br /></div>
Leonidas
http://courses.cs.taltech.ee/w/index.php?title=ITI8610&diff=7808
ITI8610
2018-11-29T06:38:30Z
<p>Leonidas: /* Grading */</p>
<hr />
<div>'''Course code''': ITI8610 <br><br />
<br />
'''Lecturer''': prof. Jüri Vain <br><br />
'''Contact''': juri.vain ätt ttu.ee, ICT-418 <br><br />
'''Co-lecturer''': Leonidas Tsiopoulos <br><br />
'''Co-lecturer''': Aleksandr Lenin <br><br />
<br />
<br />
==Time and place==<br />
<br />
Lectures: Wednesdays 10:00, ICT-315 <br><br />
Labs: Wednesdays 12.00 <br><br />
* Lab supervisors:<br />
** Aleksandr Lenin (aleksandr.lenin ätt ttu.ee) - Module I<br />
** Jüri Vain (juri.vain ätt ttu.ee), Leonidas Tsiopoulos (letsio ätt ttu.ee) - Module II<br />
<br />
==News 2018==<br />
<br><br />
Deadline for submitting lab assignments of Module II -- TBA<br />
<br />
==Lecture plan==<br />
* [[Media:ITI_8610_lecture_1.pdf|Lecture 1]]: Introduction to software assurance<br />
====Module I: Assurance processes, risk management & security assurance==== ====<br />
Lecture 1: Security Risk Management<br /><br />
Lecture 2: Security Risk Management (contd.)<br /><br />
Lecture 3: Security Best Practices<br /><br />
Lecture 4: Input Validation<br /><br />
Lecture 5. Web Application Security. Cross-Site Scripting Attacks<br /><br />
<br />
====Module II: : Assured Software Analytics ====<br />
* [[Media:Module_III_Lecture_1.pdf|Module II Lecture 1]]: Design by Contract<br />
* [[Media:Module III 2nd lecture JML Specification Cases.pdf|Module II Lecture 2]]: Specification cases<br />
* [[Media:e.pdf|Module II Lecture 3]]: Multi-view contracts of cyber-physical systems<br />
* [[Media:Module III 4th lecture.pdf|Module II Lecture 4]]: JML contracts for OOP methods<br />
* [[Media:Module III 5th lecture.pdf|Module II Lecture 5]]: A Tutorial on OpenJML<br />
<br />
==Practice Assignments==<br />
====Module I: Security Assurance ====<br />
Assignment 1: Risk Analysis using the FAIR (Factor Analysis of Information Security Risk) framework<br /><br />
Assignment 2: Vulnerability Identification in Code using Static Analysis Tools<br /><br />
Assignment 3: Architectural Risk Analysis<br /><br />
Assignment 4: Web Application Exploitation<br />
<br />
====Module II ====<br />
* [[Media:HomeAssignmnet_of ModuleII.pdf|Lab instruction]]: Lab assignment plan<br />
NB!<br />
To report completed lab assignments go to web page https://ained.ttu.ee<br />
<br />
and register as user with uniID of TUT<br />
<br />
== Grading ==<br />
<br />
Each of the two modules is graded independently on the scale 0-100 points. A student must receive a positive grade in every module. Therefore, a student may obtain max 200 points for the entire course. 51%, or 101 points is the absolute minimum required to pass the course. The standard TalTech grading rules are applied to calculate the student's final grade.<br />
<br />
==Resources==<br />
<br />
https://ained.ttu.ee -- õppekeskkonas olevad materjalid<br /><br />
Gary McGraw "Software Security. Building Security In"<br /></div>
Leonidas