Formalna verifikacija C izvornog koda temeljena na CEGAR metodi (CROSBI ID 378678)
Ocjenski rad | diplomski rad
Podaci o odgovornosti
Petrušić, Marin
Bogunović, Nikola
Bogunović, Nikola
hrvatski
Formalna verifikacija C izvornog koda temeljena na CEGAR metodi
U radu je oblikovan sustav za formalnu verifikaciju C izvornog koda koji se temelji na rafiniranju apstrakcije programa vođeno protuprimjerom (CEGAR metoda). Postupak se sastoji iz nekoliko koraka. U prvom koraku potrebno je razložiti (parsirati) C program i oblikovati apstraktni model. U slijedećem koraku provodi se verifikacija modela. Ukoliko je verifikacija apstraktnog modela uspješna to se odnosi i na izvorni program. Ako verifikacija nije uspješna, provjerava se da li je generirani protuprimjer moguć u konkretnom programu ili ne. Realan protuprimjer potvrđuje pogrešku. Za nerealan protuprimjer rafinira se model kako bi se isključila mogućnost njegove pojave te se ponavlja verifikacija na novom modelu.
formalna verifikacija; provjera modela; CEGAR
nije evidentirano
engleski
Formal verification of C source code based on CEGAR method
nije evidentirano
formal verification; model checking; CEGAR
nije evidentirano
Podaci o izdanju
71
10.07.2013.
obranjeno
Podaci o ustanovi koja je dodijelila akademski stupanj
Fakultet elektrotehnike i računarstva
Zagreb