Fakultet tehničkih nauka

Predmet: Formalne metode u modelovanju softverskih sistema (17.IFE256)

Matične organizacione jedinice predmeta: Katedra za primenjene računarske nauke
Osnovne informacije:
 
Kategorija Naučno-stručni
Uža naučna oblast Primenjene računarske nauke i informatika
ESPB 6

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
Michael Huth, Mark Ryan Logic in Computer Science: Modelling and Reasoning about Systems 2004 Cambridge University Press Engleski
J. M. Spivey The Z Notation: A Reference Manual 1992 Prentice Hall Engleski
R. D. Tennent Specifying Software: A Hands-On Introduction 2002 Cambridge University Press Engleski
Predmetna aktivnost Predispitna Obavezna Broj poena
Predmetna aktivnost
Test
Predispitna
Da
Obavezna
Da
Broj poena
10.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
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
Predavanja
Predavanja
Računarske vežbe
Računarske vežbe