Naslov
Primjena apstrakcije predikata u verifikacija programske potpore
(Application of predicate abstraction in software verification)

Autori
Pazman, Tibor

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

Fakultet
Fakultet elektrotehnike i računarstva

Mjesto
Zagreb

Datum
15.06

Godina
2011

Stranica
62

Mentor
Bogunović, Nikola

Neposredni voditelj
Bogunović, Nikola

Ključne riječi
formalne metode; formalna verifikacija; apstrakcija predikata; CEGAR postupak
(formal methods; formal verification; predicate abstraction; CEGAR method)

Sažetak
U okviru oblikovanja programske potpore formalna verifikacija je značajan i težak problem. To se posebice odnosi na sustave s velikim ili beskonačnim prostorom stanja gdje su postupci tradicijske provjere modela s eksplicitnim ili simboličkim predstavljanjem stanja neuporabivi. U radu je objašnjen princip ekstrakcije jednostavnijeg modela iz izvornog programa temeljem apstrakcije predikata. Kako verifikacija na apstrahiranom modelu može generirati protuprimjer koji nije moguć u izvođenju izvornog programa, objašnjen je postupak rafiniranja modela. Primjena formalne verifikacije programske potpore temeljene na apstrakciji predikata pokazana je na nekoliko primjera.

Izvorni jezik
Hrvatski

Znanstvena područja
Računarstvo

POVEZANOST RADA