Naslov
Formalna provjera C programa
(Formal verification of C programs)

Autori
Vidačković, Ines

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

Fakultet
Fakultet elektrotehnike i računarstva

Mjesto
Zagreb

Datum
09.07

Godina
2009

Stranica
67

Mentor
Bogunović, Nikola

Neposredni voditelj
Bogunović, Nikola

Ključne riječi
Formalna verifikacija; Ograničena provjera modela; CProver; CBMC; SATABS
(Formal verification; Bounded model checking; CProver; CBMC; SATABS)

Sažetak
U završnom radu se daje kratak uvod u formalne metode u inženjerstvu programske potpore te se opisuje problem znanstvenih formalizma u provjeri računalnih programa. Provjera modela se predlaže kao jedno od mogućih rješenja tog problema. Detaljno se, kroz primjere, demonstrira korištenje programa CBMC kao posebnog alata koji primjenjuje metodu ograničene provjere modela. Opisano je kako program instalirati i koristiti za provjeru programa na grafičkom sučelju i sučelju naredbenog retka te postupak prevođenja izvornog programa u CNF formulu za provjeru svojstva. Spominju se i drugi programi dostupni u CProver sustavu za formalnu verifikaciju C programa. U sklopu SATABS programa se uvodi metoda apstrakcije za provjeru modela i pokazuje korištenje programa kroz jednostavan primjer. Pokazana je mogućnost provjere ekvivalentnosti modela pisanih programskim jezikom C i Verilogom. Na kraju je prikazan potpuni pregled obilježja ANSI-C programskog jezika implementiranih u programski sustav CProver.

Izvorni jezik
Hrvatski

Znanstvena područja
Računarstvo

POVEZANOST RADA