Naslov
Struktura i primjena MAGIC alata za verifikaciju C programa
(Structure and application of MAGIC tool for C program verification)

Autori
Krilić, Andrija

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

Fakultet
Fakultet elektrotehnike i računarstva

Mjesto
Zagreb

Datum
03.07

Godina
2012

Stranica
40

Mentor
Bogunović, Nikola

Neposredni voditelj
Bogunović, Nikola

Ključne riječi
verifikacija programa; formalna verifikacija; CEGAR
(software verification; formal verification; CEGAR)

Sažetak
MAGIC alat kao radni okvir namijenjen je analizi i rasuđivanju o programskim komponentama pisanim u C jeziku. Osnovni cilj MAGIC alata je provjera slaganja između specifikacije neke komponente i njezine implementacije. Posebna pažnja posvećuje se provjeri reaktivnih programa kao što su razne pogonske komponente (engl. device drivers). U radu je opisana struktura MAGIC alata, principi generiranja početnih formalnih modela te metode specijaliziranja i rafiniranja modela tijekom postupka. Na tipičnim primjerima realnih problema pokazana je uspješnost primjene. U zaključku sukomentirane prednosti i nedostaci prikazanog postupka verifikacije.

Izvorni jezik
Hrvatski

Znanstvena područja
Računarstvo

POVEZANOST RADA