Provjera modela C programa lijenom apstrakcijom (CROSBI ID 365042)
Ocjenski rad | sveučilišni preddiplomski završni rad
Podaci o odgovornosti
Sruk, Marijo
Bogunović, Nikola
Bogunović, Nikola
hrvatski
Provjera modela C programa lijenom apstrakcijom
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.
formalne metode; formalna verifikacija; CEGAR metoda
nije evidentirano
engleski
Model checking of C programs by lazy abstraction
nije evidentirano
formal methods; formal verification; CEGAR method
nije evidentirano
Podaci o izdanju
34
30.06.2011.
obranjeno
Podaci o ustanovi koja je dodijelila akademski stupanj
Fakultet elektrotehnike i računarstva
Zagreb
