hrvatski

Primjena apstrakcije predikata u verifikacija programske potpore

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.

formalne metode; formalna verifikacija; apstrakcija predikata; CEGAR postupak

nije evidentirano