Naslov
Provjera modela C programa lijenom apstrakcijom
(Model checking of C programs by lazy abstraction)

Autori
Sruk, Marijo

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

Fakultet
Fakultet elektrotehnike i računarstva

Mjesto
Zagreb

Datum
30.06

Godina
2011

Stranica
34

Mentor
Bogunović, Nikola

Neposredni voditelj
Bogunović, Nikola

Ključne riječi
formalne metode; formalna verifikacija; CEGAR metoda
(formal methods; formal verification; CEGAR method)

Sažetak
Formalna verifikacija provjerom modela nastoji pokazati da li model dijela programa logički zadovoljava neku određenu specifikaciju ponašanja. Uporabom skupa alata BLAST koji se temelji na generiranju protuprimjera automatiziranom apstrakcijom, pokazan je postupak provjere ispravne uporabe sučelja C programa. Apstrakcija do željene preciznosti izvodi se tijekom provjere. U uvodnom dijelu rada opisana je arhitekturua BLAST sustava. Posebnu pažnja posvećena je temeljnim principima implementiranih algoritama i ostvarenih struktura podataka. Na primjerima realne složenosti analizirama je i komentirana uporabna vrijednost BLAST sustava.

Izvorni jezik
Hrvatski

Znanstvena područja
Računarstvo

POVEZANOST RADA