Studenti ovladavaju znanjima o realnim dosezima i uporabi formalnih metoda u oblikovanju sustava. Posebice se stiču znanja o izgradnji modela ciljnog sustava, te postupcima zadovoljavanja specificiranih strukturnih i funkcijskih zahtjeva.

1. definirati i navesti pojam ispravnog rada sustava.
2. razlikovati pogrešno i ispravno ponašanje sustava.
3. primijeniti formalnu logiku u opisu (željenog) ponašanja sustava.
4. analizirati i klasificirati odziv alata za formalnu verifikaciju sustava.
5. modificirati strukturu sustava kako bi se zadovoljilo željeno ponašanje.
6. dizajnirati i integrirati ili modificirati alate za formalnu verifikaciju sustava.
7. kreirati formalne modele realnih sustava pogodne za verifikaciju.

Nasatava je organizirana kroz dva ciklusa. Prvi ciklus sastoji se od 7 tjedana predavanja i međuispita. Drugi ciklus sastoji se iz 6 tjedna predavanja i završnog ispita.

Kratke provjere (3), domaće zadaće (3), međuispit, završni ispit.

1. Administracija predmeta, primjeri pogrešaka u oblikovanju sustava. Motivacija za stjecanje znanja iz formalnih metoda u postupku oblikovanja. Klasifikacija postupaka formalne verifikacije sustava.
2. Uloga matematičke logike u specifikaciji i provjeri zahtjeva na ponašanje sustava. Propozicijska i predikatna logika. Vremenska logika CTL i Kripkeova struktura.
3. Provjera modela kritičnih programskih dijelova korištenjem sustava NuSMV. CTL vremenska logika u specifikaciji zahtjeva sustava. 1. domaća zadaća.
4. Vremenske logike LTL i CTL*. Teorija fiksne točke kod eksplicitnog izračunavanja skupova stanja. Algoritmi izračunavanja skupova stanja za vremenske formule EX, EG i EU.
5. Alat Java PathFinder za provjeru modela programa pisanih u programskom jeziku Java. Provjera čestih svojstava i pronalaženje pogrešaka u programima pisanima u Javi. 2. domaća zadaća.
6. Formalna verifikacija sklopovlja. Pregled metoda i alata. Jezik Verilog i alat VIS koji se koristi za formalnu verifikaciju sklopovlja. Provjera modela u VIS-u na nekoliko primjera.
7. Jezik JML za označavanje i formalnu verifikaciju Javinih programa. Simboličko izračunavanje skupova stanja. Priprema za međuispit.
8. Provjera znanja
9. Formalna verifikacija komunikacijskih protokola (modeliranje jezikom Promela i uporaba alata Spin) - 1.
10. Formalna verifikacija komunikacijskih protokola (modeliranje jezikom Promela i uporaba alata Spin) - 2.
11. Formalna verifikacija komunikacijskih protokola (modeliranje jezikom Promela i uporaba alata Spin) - 3. Prikaz primjera i uvod u zadatke za domaću zadaću br. 3.
12. Izgradnja reduciranih uređenih binarnih dijagrama odlučivanja (ROBDD). Algoritam ITE i implementacija ROBDD-a. Primjena ROBDD-a u provjeri modela.
13. Algoritmi za rješavanja problema zadovoljivosti skupa Booleovih formula (SAT-problem). Postupci DPLL, GRASP, Chaff i MiniSAT. Primjena u ograničenoj provjeri modela.
14. Simboličko izvršavanje programa. SMT-rješavači. Primjena SMT-rješavača u formalnoj verifikaciji programa. Kombiniranje simboličkog i konkretnog izvršavanja programa radi učinkovitog pronalaska pogrešaka u programima.
15. Završna provjera znanja