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

Kód výsledku v 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>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

čeština

Název v původním jazyce

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

Popis výsledku v původním jazyce

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ů.

Název v anglickém jazyce

Formal Verification of PLC Programs via SMV and Uppaal

Popis výsledku anglicky

Verification of PLC programs can be done by their modelling in a universal verification tool as SMV or Uppaal. This paper proposes a modelling procedure which creates a SMV or Uppaal model of PLC program given as system of logical assignments got by theAPLCTRANS algorithm. The automaton described by this assignment system is an abstraction suitable for modelling in the mentioned tools. Proposed procedure is able to model only programs, which can be proceeded by APLCTRANS, that means all programming facilities cannot be used in the modelled program. Obtained model can lead to lower computational burden than models derived from particularmodels of program elements (for instance instructions). The procedure is suitable for modelling and verification of short control programs or program fragments and functions.

Druh

A - Audiovizuální tvorba

CEP obor

JD - Využití počítačů, robotika a její aplikace

OECD FORD obor

—

Projekt

<a href="/cs/project/GD102%2F03%2FH116" target="_blank" >GD102/03/H116: TALENT - koordinovaná výchova studentů doktorských studijních programů v oblasti řídicí techniky a robotiky</a><br>

Návaznosti

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

Rok uplatnění

2005

Kód důvěrnosti údajů

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

ISBN

80-227-2235-9

Místo vydání

Bratislava

Název nakladatele resp. objednatele

—

Verze

—

Identifikační číslo nosiče

neuvedeno