Není k dispozici

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21230%2F04%3A03099013" target="_blank" >RIV/68407700:21230/04:03099013 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

SMV Verification of PLC Programs

Popis výsledku v původním jazyce

The cyclic behavior of Programmable logical controllers (PLCs) is suitable for verifying their programs as finite automata by a model checker, for instance SMV. A subset of PLC programs can be easily converted into transfer sets with the aid of APLCTransalgorithm (RIP2003) into t-assigments, which are suitable for expressing in the definition language of SMV. The paper presents the method for transforming APLCTrans results into SMV and practical applications of the algorithm are demonstrated by the elaborated example of the verification a control program for opening gates of a garage. The whole process of its verification is performed in several logical steps to provide good introducing into the whole validation process. Finally, the program is repaired to fulfill given CTL formula.In the discussion, the proposed method is compared with another approaches to demonstrate that our method gives faster results and yields lesser computable complexity.

Název v anglickém jazyce

SMV Verification of PLC Programs

Popis výsledku anglicky

The cyclic behavior of Programmable logical controllers (PLCs) is suitable for verifying their programs as finite automata by a model checker, for instance SMV. A subset of PLC programs can be easily converted into transfer sets with the aid of APLCTransalgorithm (RIP2003) into t-assigments, which are suitable for expressing in the definition language of SMV. The paper presents the method for transforming APLCTrans results into SMV and practical applications of the algorithm are demonstrated by the elaborated example of the verification a control program for opening gates of a garage. The whole process of its verification is performed in several logical steps to provide good introducing into the whole validation process. Finally, the program is repaired to fulfill given CTL formula.In the discussion, the proposed method is compared with another approaches to demonstrate that our method gives faster results and yields lesser computable complexity.

Druh

D - Stať ve sborníku

CEP obor

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

OECD FORD obor

—

Projekt

—

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2004

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ů

Název statě ve sborníku

Proceedings of the 6th International Scientific-Technical Conference on Process COntrol (Říp 2004)

ISBN

80-7194-662-1

ISSN

—

e-ISSN

—

Počet stran výsledku

1

Strana od-do

187-187

Název nakladatele

Univerzita Pardubice

Místo vydání

Pardubice

Místo konání akce

Kouty nad Desnou

Datum konání akce

8. 6. 2004

Typ akce podle státní příslušnosti

EUR - Evropská akce

Kód UT WoS článku

—