Dp 194 cz

Z DCEwiki
Skočit na navigaci Skočit na vyhledávání

Verifikace s SMV

Autor: Šprdlík Otakar

Diplomové práce 2005

Stáhnout práci v PDF

194img.gif

Formální verifikační techniky ověřují vlastností různých systémů, mimo jiné se mohou využít pro verifikaci programů programovatelných logických automatů (PLC). K~provedení verifikace PLC programů je nutné jejich modelování ve verifikačním nástroji, například SMV nebo Uppaal. Práce předkládá postup modelování programu převedeného algoritmem APLCTRANS na soustavu logických rovnic, které tvoří abstrakci vhodnou pro modelování ve zmíněných nástrojích. Zadání původně požadovalo modelování v SMV, ale rozsah byl po dohodě s vedoucím práce rozšířen i na Uppaal. Navržený postup dokáže modelovat pouze programy, které APLCTRANS umí zpracovat, to znamená programy, které využívají omezených programovacích možností. Ukazuje se však, že výsledné modely mohou vést na nižší výpočetní nároky na proces verifikace než modely vytvořené obecnějšími postupy založenými na slučování modelů jednotlivých programových elementů (např. instrukcí). Postup se hodí pro modelování a verifikaci krátkých programů nebo dílčích bloků či funkcí rozsáhlejších řídicích algoritmů.

Dp 2005 sprdlik otakar.pdf