Construction and Verification of PLC-programs by LTL-specification
<p>An approach to construction and verification of PLC-programs for discrete tasks is proposed. For the specification of a program behavior we use the linear-time temporal logic LTL. Programming is carried out in the ST-language according to an LTL-specification. The correctness analysis of an...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2013-01-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | http://mais-journal.ru/jour/article/view/181 |
| _version_ | 1828076162599878656 |
|---|---|
| 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 | <p>An approach to construction and verification of PLC-programs for discrete tasks is proposed. For the specification of a program behavior we use the linear-time temporal logic LTL. Programming is carried out in the ST-language 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 PLCprograms is shown by an example. For a discrete problem we give a ST-program, its LTL-specification and an SMV-model.</p><p><strong>A purpose</strong> of the article is to describe an approach to programming PLC, which would provide a possibility of PLC-program correctness analysis by the model checking method.</p><p>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 that 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 specification of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program, which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTL-specification of the behavior of each program variable. In addition, an SMV-model of a PLC-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV.</p> |
| first_indexed | 2024-04-11T02:10:37Z |
| format | Article |
| id | doaj.art-67314a3c26ec4149b0b461daa199412a |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-11T02:10:37Z |
| publishDate | 2013-01-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-67314a3c26ec4149b0b461daa199412a2023-01-03T02:13:09ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172013-01-01204522175Construction and Verification of PLC-programs by LTL-specificationE. V. Kuzmin0V. A. Sokolov1D. A. Ryabukhin2Ярославский государственный университет им. П. Г. ДемидоваЯрославский государственный университет им. П. Г. ДемидоваЯрославский государственный университет им. П. Г. Демидова<p>An approach to construction and verification of PLC-programs for discrete tasks is proposed. For the specification of a program behavior we use the linear-time temporal logic LTL. Programming is carried out in the ST-language 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 PLCprograms is shown by an example. For a discrete problem we give a ST-program, its LTL-specification and an SMV-model.</p><p><strong>A purpose</strong> of the article is to describe an approach to programming PLC, which would provide a possibility of PLC-program correctness analysis by the model checking method.</p><p>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 that 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 specification of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program, which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTL-specification of the behavior of each program variable. In addition, an SMV-model of a PLC-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV.</p>http://mais-journal.ru/jour/article/view/181программируемые логические контроллерытехнология программированияспецификация и верификация программ |
| spellingShingle | E. V. Kuzmin V. A. Sokolov D. A. Ryabukhin Construction and Verification of PLC-programs by LTL-specification Моделирование и анализ информационных систем программируемые логические контроллеры технология программирования спецификация и верификация программ |
| title | Construction and Verification of PLC-programs by LTL-specification |
| title_full | Construction and Verification of PLC-programs by LTL-specification |
| title_fullStr | Construction and Verification of PLC-programs by LTL-specification |
| title_full_unstemmed | Construction and Verification of PLC-programs by LTL-specification |
| title_short | Construction and Verification of PLC-programs by LTL-specification |
| title_sort | construction and verification of plc programs by ltl specification |
| topic | программируемые логические контроллеры технология программирования спецификация и верификация программ |
| url | http://mais-journal.ru/jour/article/view/181 |
| work_keys_str_mv | AT evkuzmin constructionandverificationofplcprogramsbyltlspecification AT vasokolov constructionandverificationofplcprogramsbyltlspecification AT daryabukhin constructionandverificationofplcprogramsbyltlspecification |