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 inženjering (Godina: 1, Semestar: Letnji) |
| Master akademske studije | Informacioni i analitički inženjering (Godina: 1, Semestar: Letnji) |
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.
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.
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.
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.
| Autori | Naziv | Godina | Izdavač | Jezik |
|---|---|---|---|---|
| 1992 | Engleski | |||
| 2002 | Engleski | |||
| 2004 | Engleski |
| Predmetna aktivnost | Predispitna | Obavezna | Broj poena |
|---|---|---|---|
| Predmetna aktivnost Složeni oblici vežbi |
Predispitna Da |
Obavezna Da |
Broj poena 20.00 |
| Predmetna aktivnost Usmeni deo ispita |
Predispitna Ne |
Obavezna Da |
Broj poena 30.00 |
| Predmetna aktivnost Predmetni projekat |
Predispitna Da |
Obavezna Da |
Broj poena 30.00 |
| Predmetna aktivnost Test |
Predispitna Da |
Obavezna Da |
Broj poena 10.00 |
| Predmetna aktivnost Test |
Predispitna Da |
Obavezna Da |
Broj poena 10.00 |
vanr. prof. dr Dušan Gajić
Vanredni profesor
Predavanja
vanr. prof. dr Vladimir Dimitrieski
Vanredni profesor
Predavanja
vanr. prof. dr Vladimir Dimitrieski
Vanredni profesor
Računarske vežbe
doc. dr Marko Vještica
Docent
Računarske vežbe
