Construction and Verification of PLC-programs by LTL-specification
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-spec...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2013-08-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/181 |
| _version_ | 1797877889302003712 |
|---|---|
| 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-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.A purpose 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.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. |
| first_indexed | 2024-04-10T02:25:08Z |
| format | Article |
| id | doaj.art-99ca442043624877854edc14b5391306 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:25:08Z |
| publishDate | 2013-08-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-99ca442043624877854edc14b53913062023-03-13T08:07:32ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172013-08-0120452210.18255/1818-1015-2013-4-5-22175Construction and Verification of PLC-programs by LTL-specificationE. V. Kuzmin0V. A. Sokolov1D. A. Ryabukhin2Ярославский государственный университет им. П. Г. ДемидоваЯрославский государственный университет им. П. Г. ДемидоваЯрославский государственный университет им. П. Г. Демидова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.A purpose 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.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.https://www.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 | https://www.mais-journal.ru/jour/article/view/181 |
| work_keys_str_mv | AT evkuzmin constructionandverificationofplcprogramsbyltlspecification AT vasokolov constructionandverificationofplcprogramsbyltlspecification AT daryabukhin constructionandverificationofplcprogramsbyltlspecification |