Dp 194 cz

From DCEwiki
Revision as of 00:40, 27 August 2014 by Sturcmar (talk | contribs) (Zobrazení PDF náhledů v rámečkách.)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
Jump to: navigation, search

Verifikace s SMV[edit]

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