Formalna verifikacija programske potpore

Prikazani su podaci za akademsku godinu: 2023./2024.

Nositelji

Izv. prof. dr. sc.
Alan Jović

Predavanja

Doc. dr. sc.
Frano Škopljanac-Mačina

Laboratorijske vježbe

Doc. dr. sc.
Frano Škopljanac-Mačina

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
[FER3-HR] Audiotehnologije i elektroakustika - profil
Izborni predmeti (2. semestar)
[FER3-HR] Automatika i robotika - profil
Izborni predmeti (2. semestar)
[FER3-HR] Elektroenergetika - profil
Izborni predmeti (2. semestar)
[FER3-HR] Elektroničko i računalno inženjerstvo - profil
Izborni predmeti (2. semestar)
[FER3-HR] Elektronika - profil
Izborni predmeti (2. semestar)
[FER3-HR] Elektrostrojarstvo i automatizacija - profil
Izborni predmeti (2. semestar)
[FER3-HR] Informacijsko i komunikacijsko inženjerstvo - profil
Izborni predmeti (2. semestar)
[FER3-HR] Komunikacijske i svemirske tehnologije - profil
Izborni predmeti (2. semestar)
[FER3-HR] Programsko inženjerstvo i informacijski sustavi - profil
Izborni predmeti (2. semestar)
[FER3-HR] Računalno inženjerstvo - profil
Izborni predmeti (2. semestar)
Izborni predmet profila (2. semestar)
[FER3-HR] Računalno modeliranje u inženjerstvu - profil
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

  1. razlikovati ispravno i pogrešno ponašanje programskog sustava
  2. primijeniti formalnu logiku u opisu željenog ponašanja programskog sustava
  3. analizirati odziv alata za formalnu verifikaciju programske potpore
  4. razviti jednostavni sustav za verifikaciju programa primjenjujući neki od verifikacijskih algoritama
  5. odabrati odgovarajući algoritam i alat za učinkovitu formalnu verifikaciju programske potpore ovisno od problema
  6. kreirati apstrakcije stvarnih programskih sustava pogodne za verifikaciju

Oblici nastave

Predavanja

Uživo ili online

Laboratorij

Domać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

  1. 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.
  2. Propozicijska i predikatna logika za formalnu verifikaciju. Sintaksa i semantika. Formalni sustavi: terminologija. Prirodno zaključivanje.
  3. 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.
  4. 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.
  5. Formalna verifikacija stvarnih programa. Principi podudaranja stanja i djelomičnog smanjenja poretka. Eksplozija broja stanja. Primjer Java Pathfindera.
  6. Hoareova logika i separacijska logika. Primjeri primjene.
  7. Priprema za međuispit
  8. Međuispit
  9. Predstavljanje Booleovih funkcija. BDD dijagrami. ITE algoritam.
  10. Problem zadovoljivosti. Poznati SAT-rješavači. Izrada SAT-rješavača.
  11. Problem ispitivanja zadovoljivosti u teoriji (SMT). SMT-rješavači.
  12. Primjena rješavača ograničenja u simboličkom izvršavanju programa.
  13. Suvremeni izazovi u formalnoj verifikaciji programa.
  14. Priprema za završni ispit.
  15. 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

Sličan predmet