Formalne metode u oblikovanju sustava
Opis predmeta
Matematički zasnovani postupci specifikacije, razvoja i verifikacije sklopovskih i 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. Dedukcijski sustavi. Oblici formalnih specifikacijskih jezika. Modeli izvedbe sklopovskih i programskih sustava. Specifikacija i verifikacija izračunskih i reaktivnih sustava. Postupci verifikacije dokazivanjem teorema i provjerom modela. Alati za automatiziranu formalnu verifikaciju sustava. Formalno koncepcijsko modeliranje. Primjene u različitim domenama računalnog sklopovskog i programskog inženjerstva.
Opće kompetencije
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.
Ishodi učenja
- definirati i navesti pojam ispravnog rada sustava.
- razlikovati pogrešno i ispravno ponašanje sustava.
- primijeniti formalnu logiku u opisu (željenog) ponašanja sustava.
- analizirati i klasificirati odziv alata za formalnu verifikaciju sustava.
- modificirati strukturu sustava kako bi se zadovoljilo željeno ponašanje.
- dizajnirati i integrirati ili modificirati alate za formalnu verifikaciju sustava.
- kreirati formalne modele realnih sustava pogodne za verifikaciju.
Oblici nastave
Predavanja
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.
Provjere znanjaKratke provjere (3), domaće zadaće (3), međuispit, završni ispit.
Način ocjenjivanja
Kontinuirana nastava | Ispitni rok | |||||
---|---|---|---|---|---|---|
Vrsta provjere | Prag | Udio u ocjeni | Prag | Udio u ocjeni | ||
Domaće zadaće | 0 % | 30 % | 0 % | 30 % | ||
Kratke provjere znanja | 0 % | 9 % | 0 % | 9 % | ||
Međuispit: Pismeni | 0 % | 25 % | 0 % | |||
Završni ispit: Pismeni | 0 % | 36 % | ||||
Ispit: Pismeni | 0 % | 61 % |
Tjedni plan nastave
- Administracija predmeta, primjeri pogrešaka u oblikovanju sustava. Motivacija za stjecanje znanja iz formalnih metoda u postupku oblikovanja. Klasifikacija postupaka formalne verifikacije sustava.
- Uloga matematičke logike u specifikaciji i provjeri zahtjeva na ponašanje sustava. Propozicijska i predikatna logika. Vremenska logika CTL i Kripkeova struktura.
- Provjera modela kritičnih programskih dijelova korištenjem sustava NuSMV. CTL vremenska logika u specifikaciji zahtjeva sustava. 1. domaća zadaća.
- 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.
- 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.
- 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.
- Jezik JML za označavanje i formalnu verifikaciju Javinih programa. Simboličko izračunavanje skupova stanja. Priprema za međuispit.
- Provjera znanja
- Formalna verifikacija komunikacijskih protokola (modeliranje jezikom Promela i uporaba alata Spin) - 1.
- Formalna verifikacija komunikacijskih protokola (modeliranje jezikom Promela i uporaba alata Spin) - 2.
- 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.
- Izgradnja reduciranih uređenih binarnih dijagrama odlučivanja (ROBDD). Algoritam ITE i implementacija ROBDD-a. Primjena ROBDD-a u provjeri modela.
- Algoritmi za rješavanja problema zadovoljivosti skupa Booleovih formula (SAT-problem). Postupci DPLL, GRASP, Chaff i MiniSAT. Primjena u ograničenoj provjeri modela.
- 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.
- Završna provjera znanja
Studijski programi
Sveučilišni diplomski
Obradba informacija (profil)
Teorijski predmeti profila
(2. semestar)
Programsko inženjerstvo i informacijski sustavi (profil)
Teorijski predmeti profila
(2. semestar)
Računalno inženjerstvo (profil)
Teorijski predmeti profila
(2. semestar)
Računarska znanost (profil)
Teorijski predmeti profila
(2. semestar)
Telekomunikacije i informatika (profil)
Teorijski predmeti profila
(2. semestar)
Literatura
Izvedba
ID 34401
Ljetni semestar
5 ECTS
R1 Engleski jezik
R1 E-učenje
45 Predavanja
0 Auditorne vježbe
0 Laboratorijske vježbe
0 Konstrukcijske vježbe
Ocjenjivanje
88 izvrstan
73 vrlo dobar
58 dobar
50 dovoljan