Construction and Verification of PLC LD-programs by LTL-specification
An approach to construction and verification of PLC LD-programs for discrete problems is proposed. For the specification of the program behavior, we use the linear-time temporal logic LTL. Programming is carried out in the LD-language (Ladder Diagram) according to an LTL-specification. The correctne...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2013-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/159 |
| _version_ | 1797877895256866816 |
|---|---|
| author | E. V. Kuzmin V. A. Sokolov D. A. Ryabukhin |
| author_facet | E. V. Kuzmin V. A. Sokolov D. A. Ryabukhin |
| author_sort | E. V. Kuzmin |
| collection | DOAJ |
| description | An approach to construction and verification of PLC LD-programs for discrete problems is proposed. For the specification of the program behavior, we use the linear-time temporal logic LTL. Programming is carried out in the LD-language (Ladder Diagram) according to an LTL-specification. The correctness analysis of an LTL-specification is carried out by the symbolic model checking tool Cadence SMV. A new approach to programming and verification of PLC LD-programs is shown by an example. For a discrete problem, we give a LD-program, its LTL-specification and an SMV-model. The purpose of the article is to describe an approach to programming PLC, which would provide a possibility of LD-program correctness analysis by the model checking method. Under the proposed approach, the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations which increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value. The LTL-formulas (used for speci- fication of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program (LD-program), which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTLspecification of the behavior of each program variable. In addition, an SMV-model of a PLC LD-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV. |
| first_indexed | 2024-04-10T02:25:14Z |
| format | Article |
| id | doaj.art-b3b4a373072a44f8ba9fc1dc9a07e541 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:25:14Z |
| publishDate | 2013-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-b3b4a373072a44f8ba9fc1dc9a07e5412023-03-13T08:07:32ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172013-12-01206789410.18255/1818-1015-2013-6-78-94153Construction and Verification of PLC LD-programs by LTL-specificationE. V. Kuzmin0V. A. Sokolov1D. A. Ryabukhin2Ярославский государственный университет им. П. Г. ДемидоваЯрославский государственный университет им. П. Г. ДемидоваЯрославский государственный университет им. П. Г. ДемидоваAn approach to construction and verification of PLC LD-programs for discrete problems is proposed. For the specification of the program behavior, we use the linear-time temporal logic LTL. Programming is carried out in the LD-language (Ladder Diagram) according to an LTL-specification. The correctness analysis of an LTL-specification is carried out by the symbolic model checking tool Cadence SMV. A new approach to programming and verification of PLC LD-programs is shown by an example. For a discrete problem, we give a LD-program, its LTL-specification and an SMV-model. The purpose of the article is to describe an approach to programming PLC, which would provide a possibility of LD-program correctness analysis by the model checking method. Under the proposed approach, the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations which increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value. The LTL-formulas (used for speci- fication of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program (LD-program), which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTLspecification of the behavior of each program variable. In addition, an SMV-model of a PLC LD-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV.https://www.mais-journal.ru/jour/article/view/159программируемые логические контроллерытехнология программированияспецификация и верификация программрелейные диаграммы |
| spellingShingle | E. V. Kuzmin V. A. Sokolov D. A. Ryabukhin Construction and Verification of PLC LD-programs by LTL-specification Моделирование и анализ информационных систем программируемые логические контроллеры технология программирования спецификация и верификация программ релейные диаграммы |
| title | Construction and Verification of PLC LD-programs by LTL-specification |
| title_full | Construction and Verification of PLC LD-programs by LTL-specification |
| title_fullStr | Construction and Verification of PLC LD-programs by LTL-specification |
| title_full_unstemmed | Construction and Verification of PLC LD-programs by LTL-specification |
| title_short | Construction and Verification of PLC LD-programs by LTL-specification |
| title_sort | construction and verification of plc ld programs by ltl specification |
| topic | программируемые логические контроллеры технология программирования спецификация и верификация программ релейные диаграммы |
| url | https://www.mais-journal.ru/jour/article/view/159 |
| work_keys_str_mv | AT evkuzmin constructionandverificationofplcldprogramsbyltlspecification AT vasokolov constructionandverificationofplcldprogramsbyltlspecification AT daryabukhin constructionandverificationofplcldprogramsbyltlspecification |