Formal Verification of PLC Programs via SMV and Uppaal

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F05%3A03109506" target="_blank" >RIV/68407700:21230/05:03109506 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

čeština

Original language name

Formální verifikace PLC programů pomocí SMV a Uppaal

Original language description

K provedení formální verifikace PLC programu je nutné jeho modelování ve verifikačním nástroji, například SMV nebo Uppaal. K modelování je možné využít převod programu algoritmem APLCTRANS na množinu logických prirazení. Postupem, který využívá tohoto algoritmu, lze modelovat pouze programy, které umí použitý algoritmus 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é obecnejší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ů.

Czech name

Formální verifikace PLC programů pomocí SMV a Uppaal

Czech description

K provedení formální verifikace PLC programu je nutné jeho modelování ve verifikačním nástroji, například SMV nebo Uppaal. K modelování je možné využít převod programu algoritmem APLCTRANS na množinu logických prirazení. Postupem, který využívá tohoto algoritmu, lze modelovat pouze programy, které umí použitý algoritmus 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é obecnejší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ů.

Type

A - Audiovisual production

CEP classification

JD - Use of computers, robotics and its application

OECD FORD branch

—

Project

<a href="/en/project/GD102%2F03%2FH116" target="_blank" >GD102/03/H116: TALENT - coordinated education of Ph. D. students in control engineering and robotics</a><br>

Continuities

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Publication year

2005

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

ISBN

80-227-2235-9

Place of publication

Bratislava

Publisher/client name

—

Version

—

Carrier ID

neuvedeno