Formalna verifikacija programske potpore
Prikazani su podaci za akademsku godinu: 2023./2024.
Nositelji
Predavanja
Laboratorijske vježbe
Opis predmeta
Matematički zasnovani postupci specifikacije, razvoja i verifikacije programskih sustava s ciljem poboljšanja kvalitete završnog proizvoda uz istovremeno smanjivanje vremena stavljanja proizvoda na tržište. Vremenska logika i njezini oblici. Specifikacija i verifikacija izračunskih i reaktivnih sustava. Formalna verifikacija stvarnih programa. Principi apstrakcije i simboličke verifikacije. Hoareova logika i separacijska logika. Algoritmi verifikacije dokazivanjem teorema i provjerom modela: binarni dijagrami odlučivanja, SAT-rješavači, SMT-rješavači. Alati za automatiziranu formalnu verifikaciju programske potpore. Primjene u različitim domenama programskog inženjerstva.
Studijski programi
Sveučilišni diplomski
Izborni predmeti (2. semestar)[FER3-HR] Automatika i robotika - profil
Izborni predmeti
(2. semestar)
[FER3-HR] Elektroenergetika - profil
Izborni predmeti
(2. semestar)
Izborni predmeti
(2. semestar)
[FER3-HR] Elektronika - profil
Izborni predmeti
(2. semestar)
Izborni predmeti
(2. semestar)
Izborni predmeti
(2. semestar)
Izborni predmeti
(2. semestar)
Izborni predmeti
(2. semestar)
[FER3-HR] Računalno inženjerstvo - profil
Izborni predmeti
(2. semestar)
Izborni predmet profila
(2. semestar)
Izborni predmeti
(2. semestar)
[FER3-HR] Računarska znanost - profil
Jezgreni predmeti profila
(2. semestar)
[FER3-HR] Znanost o mrežama - profil
Izborni predmeti
(2. semestar)
[FER3-HR] Znanost o podacima - profil
Izborni predmeti
(2. semestar)
[FER2-HR] Obradba informacija - profil
Teorijski predmeti profila
(2. semestar)
[FER2-HR] Programsko inženjerstvo i informacijski sustavi - profil
Teorijski predmeti profila
(2. semestar)
[FER2-HR] Računalno inženjerstvo - profil
Teorijski predmeti profila
(2. semestar)
[FER2-HR] Računarska znanost - profil
Teorijski predmeti profila
(2. semestar)
[FER2-HR] Telekomunikacije i informatika - profil
Teorijski predmeti profila
(2. semestar)
Ishodi učenja
- razlikovati ispravno i pogrešno ponašanje programskog sustava
- primijeniti formalnu logiku u opisu željenog ponašanja programskog sustava
- analizirati odziv alata za formalnu verifikaciju programske potpore
- razviti jednostavni sustav za verifikaciju programa primjenjujući neki od verifikacijskih algoritama
- odabrati odgovarajući algoritam i alat za učinkovitu formalnu verifikaciju programske potpore ovisno od problema
- kreirati apstrakcije stvarnih programskih sustava pogodne za verifikaciju
Oblici nastave
Predavanja
Uživo ili online
LaboratorijDomaće zadaće
Način ocjenjivanja
Kontinuirana nastava | Ispitni rok | |||||
---|---|---|---|---|---|---|
Vrsta provjere | Prag | Udio u ocjeni | Prag | Udio u ocjeni | ||
Domaće zadaće | 40 % | 40 % | 40 % | 40 % | ||
Međuispit: Pismeni | 0 % | 30 % | 0 % | |||
Završni ispit: Pismeni | 0 % | 30 % | ||||
Ispit: Pismeni | 33 % | 60 % |
Tjedni plan nastave
- Uvod u formalnu verifikaciju programske potpore. Uloga tehnika formalne specifikacije i analize u životnom ciklusu programske potpore. Jezici za iskazivanje tvrdnji u programima i pristupi analizi tvrdnji. Formalni pristupi modeliranju i analizi programske potpore. Alati za potporu formalnim metodama. Specifikacijski jezici, jezici za ispitivanje i jezici za verifikaciju.
- Propozicijska i predikatna logika za formalnu verifikaciju. Sintaksa i semantika. Formalni sustavi: terminologija. Prirodno zaključivanje.
- Vremenska logika CTL za verifikaciju reaktivne programe. Provjera modela za reaktivnu programsku potporu. Automatsko i na automatima temeljeno programiranje za istovremene sustave. Komunicirajući procesi, provjera pravednosti. Sustav NuSMV / NuXMV.
- Vremenske logike LTL i CTL* za verifikaciju reaktivne programske potpore. Provjera modela za reaktivnu programsku potporu. Automatsko i na automatima temeljeno programiranje za istovremene sustave.
- Formalna verifikacija stvarnih programa. Principi podudaranja stanja i djelomičnog smanjenja poretka. Eksplozija broja stanja. Primjer Java Pathfindera.
- Hoareova logika i separacijska logika. Primjeri primjene.
- Priprema za međuispit
- Međuispit
- Predstavljanje Booleovih funkcija. BDD dijagrami. ITE algoritam.
- Problem zadovoljivosti. Poznati SAT-rješavači. Izrada SAT-rješavača.
- Problem ispitivanja zadovoljivosti u teoriji (SMT). SMT-rješavači.
- Primjena rješavača ograničenja u simboličkom izvršavanju programa.
- Suvremeni izazovi u formalnoj verifikaciji programa.
- Priprema za završni ispit.
- Završni ispit
Literatura
(.), Mordechai Ben-Ari (2012.), Mathematical Logic for Computer Science, Springer,
(.), Daniel Kroening, Ofer Strichman (2016.), Decision Procedures: An Algorithmic Point of View, 2nd Ed., Springer,
(.), Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh (2021.), Handbook of Satisfiability, 2nd Ed., IOS Press, 2021.,
(.), Klaus Schneider (2010.), Verification of Reactive Systems: Formal Methods and Algorithms, Springer,
(.), Michael Huth, Mark Ryan (2004.), Logic in Computer Science, Cambridge University Press,
(.), S. Demri, V. Goranko, M. Lange, Temporal Logics in Computer Science: Finite State Systems, Cambridge University Press, 2016.,
Za studente
Izvedba
ID 222519
Ljetni semestar
5 ECTS
R0 Engleski jezik
R1 E-učenje
45 Predavanja
0 Seminar
0 Auditorne vježbe
13 Laboratorijske vježbe
0 Konstrukcijske vježbe
0 Vježbe tjelesnog odgoja
Ocjenjivanje
88 izvrstan
75 vrlo dobar
63 dobar
50 dovoljan