Predmet: Formalne metode u modelovanju softverskih sistema (17.IFE256 )
Matične organizacione jedinice predmeta: Katedra za primenjene računarske nauke
Studijski programi predmeta:
| Stepen i vrsta studija | Naziv |
|---|---|
| Master akademske studije | Informacioni i analitički inženjering (Godina: 1, Letnji) |
| Master akademske studije | Informacioni inženjering (Godina: 1, Letnji) |
Cilj:
Obrazovanje studenata u oblasti formalnih metoda u modelovanju softverskih sistema i sistema u kojima se primenjuje softver. Ovladavanje pristupima i tehnikama primene formalnih metoda u modelovanju softverskih sistema i sistema u kojima se primenjuje softver.
Ishod:
Po završetku kursa studenti će biti osposobljeni da: • Koriste matematičke koncepte tipa skupa, skupa sa duplikatima, funkcije i relacije, u cilju formalne specifikacije softverskih sistema i njihovih karakteristika. • Vrše proveru formalnih specifikacija, proveru modela i dokazuju zadovoljenje zahtevanih osobina softverskih sistema. • Koriste matematičko razmišljanje za dokazivanje zadovoljenja osobina softverskih modela. • Kreiraju specifikacije transformacija modela, odnosno generatore programskog koda iz specifikacija, i u jednostavnijim slučajevima izvrše formalnu proveru generisanog koda.
Sadržaj:
Uvod u formalne metode. Z notacija. Hoareova logika i verifikacija programa. Hoareove trojke. Delimična i potpuna korektnost. Dokazivanje delimične korektnosti. Najslabiji preduslovi i automatska verifikacija. Primena temporalne logike i drugih vrsta logika u modelovanju sistema i proveri modela. Temporalna logika u linearnom vremenu (TLLV). Provera modela primenom pristupa zasnovanog na teoriji automata. Provera modela zasnovana na primeni TLLV.
Metodologija izvođenja nastave:
Nastava se izvodi u obliku predavanja, auditornih i računarskih vežbi (u računarskoj laboratoriji) i konsultacija. Tokom celokupnog procesa izvođenja nastave, studenti se podstiču na intenzivnu komunikaciju, kritičko rezonovanje, samostalni rad i aktivan odnos prema procesu nastave. Uslov za dobijanje potpisa i izlazak na završni ispit predstavlja izvršenje svih predispitnih obaveza, u minimalnom obimu od 30 poena.
Literatura:
| Autori | Naziv | Godina | Izdavač | Jezik |
|---|---|---|---|---|
| 2002 | Engleski | |||
| 2004 | Engleski | |||
| 1992 | Engleski |
Formiranje ocene:
| Predmetna aktivnost | Predispitna | Obavezna | Broj poena |
|---|---|---|---|
| Test | Da | Da | 10.00 |
| Usmeni deo ispita | Ne | Da | 30.00 |
| Predmetni projekat | Da | Da | 30.00 |
| Složeni oblici vežbi | Da | Da | 20.00 |
| Test | Da | Da | 10.00 |
Izvođači nastave:
vanr. prof. dr Gajić Dušan
Vanredni profesor
Predavanja
Asistent dr Vještica Marko
Asistent
Računarske vežbe
vanr. prof. dr Dimitrieski Vladimir
Vanredni profesor
Računarske vežbe
vanr. prof. dr Dimitrieski Vladimir
Vanredni profesor
