SMV Verification of PLC Programs

Result code in 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>
Result on the web
—
DOI - Digital Object Identifier
—

Result language
angličtina
Original language name
SMV Verification of PLC Programs
Original language description
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.
Czech name
Není k dispozici
Czech description
Není k dispozici

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

Article name in the collection
Proceedings of the 6th International Scientific-Technical Conference on Process COntrol (Říp 2004)
ISBN
80-7194-662-1
ISSN
—
e-ISSN
—
Number of pages
1
Pages from-to
187-187
Publisher name
Univerzita Pardubice
Place of publication
Pardubice
Event location
Kouty nad Desnou
Event date
Jun 8, 2004
Type of event by nationality
EUR - Evropská akce
UT code for WoS article
—

Similar results(10)