Naslov
Formalna verifikacija C izvornog koda temeljena na CEGAR metodi
(Formal verification of C source code based on CEGAR method)

Autori
Petrušić, Marin

Vrsta, podvrsta i kategorija rada
Ocjenski radovi, diplomski rad, diplomski

Fakultet
Fakultet elektrotehnike i računarstva

Mjesto
Zagreb

Datum
10.07

Godina
2013

Stranica
71

Mentor
Bogunović, Nikola

Neposredni voditelj
Bogunović, Nikola

Ključne riječi
formalna verifikacija; provjera modela; CEGAR
(formal verification; model checking; CEGAR)

Sažetak
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.

Izvorni jezik
Hrvatski

Znanstvena područja
Računarstvo

POVEZANOST RADA