Kursuse eesmärk on anda alusteadmised tarkvara arenduses kasutatavatest fomaalmeetoditest. Klassikalised arendusmeetodid ei ole enam piisavad tagamaks ohutus- ja turvakriitiliste tarkvarasüsteemide korrektset nõuete spetsifitseerimist, kavandamist ja implementeerimist. Kursus annab vajalikud baasteadmised põhilistest arendussammude automaatiseerimise tehnikatest ja praktilised oskused arendusvahendite kasutamiseks. Käsitletakse sünteesi ja verifitseerimise (sh mudelipõhise testimise, mudelkontrolli ja deduktiivse verifitseerimise) tehnikaid objekt-orienteeritud, ajakitsendustega ja hajustarkvara arenduses.

The goal is to provide the basics of formal methods applied in contemporary software engineering practice. Classical schematics based methods alone do not guarantee the quality of software products regarding safety, security and functional correctness requirements. The aims at providing theoretical knowledge and practical skills needed for applying formal techniques and tools in software development automation.

Kursuse edukas läbimine annab oskused iseseisvalt:
a. koostada ja verifitseerida tarkvara nõuete spetsifikatsioone;
b. kasutades mudelkontrolli ja deduktiivse verifitseerimise vahendeid valideerida arendussammude korrektsust nõuete suhtes;
c. kasutada mudelipõhise testigenereerimise ja -täitmise tehnikaid ja keskkondi;
d. mõistma ja kasutama korrektsust tagavaid tarkvara sünteesimeetodeid (correct by construction synthesis).

Passing the course provides basic knowledge and skills for
a. composing and verifying software requirements specifications
b. performing and validating the correctness of development steps by using model checking and deductive verification tools
c. using model based development techniques and tools for automated test generation and execution.

Kursus eeldab esmateadmisi algoritmikast, loogikast, andmestruktuuridest ja programmeerimisest.
Kursus katab järgmisi teemasid:
a. tarkvara mudelid ja semantika: olekud vs sündmused, determinism vs mittedeterminism, sünkroonsus vs asünkroonsus, ohutus vs elusus, reaalaeg ja hajussüsteemid;
b. Mudelteisendustel ja kitsenduste lahendamisel põhinev tarkvara süntees, korrektsust säilitavad teisendused.
c. Verifitseerimisalgoritmid mudelkontrollis ja deduktiivses verifitseerimises.
d. Verifitseerimistehnikad: olekuruumi redutseerimine, aspekt-orienteeritud ja komponentmudelid, kompositsiooniline ja hiearhiline verifitseerimine, abstraktsioon.
e. Arendusvahendid: Key, Z3, Rodin, Uppaal.

As a prerequisite the course presumes basic knowledge in algorithmics, logics, data structures and programming. The main body of the course covers:
a. Software models and their semantics: state vs event-based, deterministic vs non-deterministic, synchronous vs asynchronous, safety, liveness, real time and concurrency.
b. Correctness preserving model transformation- and constraint solving based software synthesis
c. Verification algorithms in model checking and in deductive verification
d. Verification techniques: state space reduction, aspect- oriented, and component models, compositional and hierarchical verification, abstractions.

Aine läbimise eelduseks on praktikumiülesannete ja kodutöö õigeaegne esitamine ja kaitsmine praktikumides ning kolme testi ja eksami sooritamine vähemalt hindele 1. Mittesooritatud testide korral tuleb sooritada koondtest positiivsele hindele (1-5). Testide tulemused mõjutavad koondhinnet kaaluga 2/5 ja eksamihinne kaaluga 2/5 ja kodutöö kaaluga 1/5.
Praktikum: Kursus sisaldab kokku 6 praktikumiülesannet eelmises loengus läbitud teema teadmiste kinnistamiseks. Praktikumi ülesanneteks on formaalne modelleerimine ja verifitseerimine kasutades loengus omandatud teoreetilisi teadmisi. Praktikumi ülesanded tuleb lahendada individuaalselt, tulemused esitada Moodle's hiljemalt järgmise praktikumi alguseks ja kaitsta suuliselt hiljemalt järgmise praktikumi jooksul.
Kodutöö: Kodutööks on rakenduslikud verifitseerimis/-mudelipõhise testimise ülesanded, mis on mahukamad praktikumiülesannetest. Kodutöö on kohustuslik ja tulemus peab olema esitatud semestri lõpus vastavalt selleks määratud tähtajaks. Kodutööde hindamine ja tagasiside andmine toimub peale esitamistähtaega 1 nädala jooksul.
Testid: Semestri jooksul tuleb selleks määratud aegadel sooritada 3 kirjalikku testi tulemusega 1-5 palli. Testi ebaõnnestumise korral on võimalik sooritada see järeltööna semestri lõpus.
Koondtest: Kui üks test ebaõnnestub mitu korda või mitu testi ebaõnnestub, siis tuleb koondhinde saamiseks sooritada koondtest. Koondtest võib katta kogu kursuse materjali. Koondtesti saavad sooritada ka need, kes soovivad parandada oma eelnevate testide tulemusi.
Koondhinne arvutatakse testide, kodutöö ja eksami hinnete kaalutud keskmisena. Kaalud: 3 * test - a' 2/15 (või koondtest - 2/5), eksam - 2/5 ja kodutöö - 1/5.

Prerequisites of passing the course are timely reporting of home assignment, lab assignments and passing tests each with mark not less than "1". In case any test fails the concluding test has to be done with positive mark (1-5). The weights of marks in calculating the final mark are following: test - 2/15 (or concluding test - 2/5), exam - 2/5, home assignment - 1/5).
Lab assignments: The course includes 6 lab assignments each of them on the topic passed in the previous lecture. Assignments have to be accomplished individually, submitted in Moodle and defended orally in the presence of lab supervisor latest during the next lab after giving the assignement.
Home assignment: Home assignement is obligatory prerequisite for assessment and it includes practical verification/- model-based testing task that is more complex than lab assignment. Report of home assignment has to be presented before the semester end meet the given deadline. Feedback on assignment mark will be given within one week.
Tests: There are 3 tests to be passed with positive score (marks 1-5). If any of the tests failes it has to be repeated in the end of semester. In case more than one test or many attempts of the same test fail Concluding test has to be passed with positive score.
Concluding Test: Concluding test is required in case several tests fail or student wants to improve his/her final score. Concluding test may cover all the material tought during the course.
Final mark is calculated as weighted average of test scores, home assignment and final exam provided the individual tests or concluding test (improving result) are positive (1 - 5). The weights are following: test - 2/15 (or concluding test - 2/5, exam - 2/5, home assignment - 1/5).

Täiendava materjaliga tutvumine ja verifitseerimis/-mudelipõhise testimise koduülesanne, mis on mahukamad praktikumiülesannetest. Kodutöö on kohustuslik ja tulemus peab olema esitatud semestri lõpus vastavalt selleks määratud tähtajaks. Kodutööde hindamine ja tagasiside andmine toimub peale esitamistähtaega 1 nädala jooksul.

Reading the papers and textbooks referred in the course web page and solving the home assignement that includes practical verification/- model-based testing task. Report of home assignment has to be presented before the semester end meet the given deadline. Feedback on assignment mark will be given within one week.

Kursuse veebileht: https://courses.cs.ttu.ee/pages/ITI8531
a. Alur & Henzinger, Computer-aided verification, 1999.
b. Ch.Baier&J.-P.Katoen. Principles of Model Checking. MIT Press 2008, 975 pages.
c. J.R.Abrial. The Book: Assigning Programs to Meanings, 2010. DOI: http://dx.doi.org/10.1017/CBO9780511624162

-