On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification
The article is devoted to the approach to constructing and verification of discrete PLC-programs by LTL-specification. This approach provides an ability of correctness analysis of PLC-programs by the model checking method. The linear temporal logic LTL is used as a language of specification of the prog...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2015-08-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/269 |
| _version_ | 1797877910248357888 |
|---|---|
| author | E. V. Kuzmin D. A. Ryabukhin V. A. Sokolov |
| author_facet | E. V. Kuzmin D. A. Ryabukhin V. A. Sokolov |
| author_sort | E. V. Kuzmin |
| collection | DOAJ |
| description | The article is devoted to the approach to constructing and verification of discrete PLC-programs by LTL-specification. This approach provides an ability of correctness analysis of PLC-programs by the model checking method. The linear temporal logic LTL is used as a language of specification of the program behavior. The correctness analysis of LTL-specification is automatically performed by the symbolic model checking tool Cadence SMV. The article demonstrates the consistency of the approach to constructing and verification of PLC programs by LTL-specification from the point of view of Turing power. It is proved, that in accordance with this approach for any Minsky counter machine can be built an LTL-specification, which is used for machine implementation in any PLC programming language of standard IEC 61131-3. Minsky machines equipollent Turing machines, and the considered approach also has Turing power. The proof focuses on representation of a counter machine behavior in the form of a set of LTL-formulas and matching these formulas to constructions of ST and SFC languages. SFC is interesting as a specific graphical language. ST is considered as a basic language because an implementation of a counter machine in IL, FBD/CFC and LD languages is reduced to rewriting blocks of ST-program. The idea of the proof is demonstrated by an example of a Minsky 3-counter machine, which implements a function of squaring. |
| first_indexed | 2024-04-10T02:24:22Z |
| format | Article |
| id | doaj.art-e00f2c0476764f68b8de26624f3e8178 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:24:22Z |
| publishDate | 2015-08-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-e00f2c0476764f68b8de26624f3e81782023-03-13T08:07:34ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172015-08-0122450752010.18255/1818-1015-2015-4-507-520255On the Expressiveness of the Approach to Constructing PLC-programs by LTL-SpecificationE. V. Kuzmin0D. A. Ryabukhin1V. A. Sokolov2Ярославский государственный университет им. П.Г. ДемидоваЯрославский государственный университет им. П.Г. ДемидоваЯрославский государственный университет им. П.Г. ДемидоваThe article is devoted to the approach to constructing and verification of discrete PLC-programs by LTL-specification. This approach provides an ability of correctness analysis of PLC-programs by the model checking method. The linear temporal logic LTL is used as a language of specification of the program behavior. The correctness analysis of LTL-specification is automatically performed by the symbolic model checking tool Cadence SMV. The article demonstrates the consistency of the approach to constructing and verification of PLC programs by LTL-specification from the point of view of Turing power. It is proved, that in accordance with this approach for any Minsky counter machine can be built an LTL-specification, which is used for machine implementation in any PLC programming language of standard IEC 61131-3. Minsky machines equipollent Turing machines, and the considered approach also has Turing power. The proof focuses on representation of a counter machine behavior in the form of a set of LTL-formulas and matching these formulas to constructions of ST and SFC languages. SFC is interesting as a specific graphical language. ST is considered as a basic language because an implementation of a counter machine in IL, FBD/CFC and LD languages is reduced to rewriting blocks of ST-program. The idea of the proof is demonstrated by an example of a Minsky 3-counter machine, which implements a function of squaring.https://www.mais-journal.ru/jour/article/view/269программируемые логические контроллеры (плк)построение и верификация плк-программltl-спецификациясчётчиковые машины минского |
| spellingShingle | E. V. Kuzmin D. A. Ryabukhin V. A. Sokolov On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification Моделирование и анализ информационных систем программируемые логические контроллеры (плк) построение и верификация плк-программ ltl-спецификация счётчиковые машины минского |
| title | On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification |
| title_full | On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification |
| title_fullStr | On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification |
| title_full_unstemmed | On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification |
| title_short | On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification |
| title_sort | on the expressiveness of the approach to constructing plc programs by ltl specification |
| topic | программируемые логические контроллеры (плк) построение и верификация плк-программ ltl-спецификация счётчиковые машины минского |
| url | https://www.mais-journal.ru/jour/article/view/269 |
| work_keys_str_mv | AT evkuzmin ontheexpressivenessoftheapproachtoconstructingplcprogramsbyltlspecification AT daryabukhin ontheexpressivenessoftheapproachtoconstructingplcprogramsbyltlspecification AT vasokolov ontheexpressivenessoftheapproachtoconstructingplcprogramsbyltlspecification |