Formalna verifikacija programske potpore

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. Matematička logika kao temelj specifikacijskih jezika. Vremenska logika i njezini oblici. Specifikacija i verifikacija izračunskih i reaktivnih sustava. Principi apstrakcije i simboličke verifikacije. 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.

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. 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.
  3. 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.
  4. Formalna verifikacija stvarnih programa. Principi podudaranja stanja i djelomičnog smanjenja poretka. Eksplozija broja stanja. Primjer Java Pathfindera.
  5. Apstraktna interpretacija i apstrakcija predikata. Apstrakcija programa, rafiniranje apstrakcije, metoda CEGAR.
  6. Hoareova logika i separacijska logika. Primjeri primjene.
  7. Priprema za međuispit
  8. Međuispit
  9. Problem zadovoljivosti. Poznati SAT-rješavači. Izrada SAT-rješavača
  10. Predstavljanje Booleovih funkcija. BDD dijagrami. ITE algoritam.
  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

Studijski programi

Sveučilišni diplomski
Audiotehnologije i elektroakustika (profil)
Slobodni izborni predmeti (2. semestar)
Automatika i robotika (profil)
Slobodni izborni predmeti (2. semestar)
Elektroenergetika (profil)
Slobodni izborni predmeti (2. semestar)
Elektroničko i računalno inženjerstvo (profil)
Slobodni izborni predmeti (2. semestar)
Elektronika (profil)
Slobodni izborni predmeti (2. semestar)
Elektrostrojarstvo i automatizacija (profil)
Slobodni izborni predmeti (2. semestar)
Informacijsko i komunikacijsko inženjerstvo (profil)
Slobodni izborni predmeti (2. semestar)
Komunikacijske i svemirske tehnologije (profil)
Slobodni izborni predmeti (2. semestar)
Programsko inženjerstvo i informacijski sustavi (profil)
Slobodni izborni predmeti (2. semestar)
Računalno inženjerstvo (profil)
Izborni predmet profila (2. semestar)
Računalno modeliranje u inženjerstvu (profil)
Slobodni izborni predmeti (2. semestar)
Računarska znanost (profil)
Jezgreni predmeti profila (2. semestar)
Znanost o mrežama (profil)
Slobodni izborni predmeti (2. semestar)
Znanost o podacima (profil)
Slobodni izborni predmeti (2. semestar)

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,
(.), Christel Baier, Joost Pieter Katoen (2008.), Principles of Model Checking, MIT Press,
(.), 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
13 Laboratorijske vježbe

Ocjenjivanje

88 izvrstan
75 vrlo dobar
63 dobar
50 dovoljan