Temporal Logic for Programmable Logic Controllers
We address the formal verification of the control software of critical systems, i.e., ensuring the absence of design errors in a system with respect to requirements. Control systems are usually based on industrial controllers, also known as Programmable Logic Controllers (PLCs). A specific feature o...
| Main Authors: | , , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2020-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1433 |
| _version_ | 1826558913091207168 |
|---|---|
| author | Natalia Olegovna Garanina Igor Sergeevich Anureev Vladimir Evgenyevich Zyubin Sergey Mikhailovich Staroletov Tatiana Victorovna Liakh Andrey Sergeevich Rozov Sergei Petrovich Gorlatch |
| author_facet | Natalia Olegovna Garanina Igor Sergeevich Anureev Vladimir Evgenyevich Zyubin Sergey Mikhailovich Staroletov Tatiana Victorovna Liakh Andrey Sergeevich Rozov Sergei Petrovich Gorlatch |
| author_sort | Natalia Olegovna Garanina |
| collection | DOAJ |
| description | We address the formal verification of the control software of critical systems, i.e., ensuring the absence of design errors in a system with respect to requirements. Control systems are usually based on industrial controllers, also known as Programmable Logic Controllers (PLCs). A specific feature of a PLC is a scan cycle: 1) the inputs are read, 2) the PLC states change, and 3) the outputs are written. Therefore, in order to formally verify PLC, e.g., by model checking, it is necessary to describe the transition system taking into account this specificity and reason both in terms of state transitions within a cycle and in terms of larger state transitions according to the scan-cyclic semantics. We propose a formal PLC model as a hyperprocess transition system and temporal cycle-LTL logic based on LTL logic for formulating PLC property. A feature of the cycle-LTL logic is the possibility of viewing the scan cycle in two ways: as the effect of the environment (in particular, the control object) on the control system and as the effect of the control system on the environment. For both cases we introduce modified LTL temporal operators. We also define special modified LTL temporal operators to specify inside properties of scan cycles. We describe the translation of formulas of cycle-LTL into formulas of LTL, and prove its correctness. This implies the possibility ofmodel checking requirements expressed in logic cycle-LTL, by using well-known model checking tools with LTL as specification logic, e.g., Spin. We give the illustrative examples of requirements expressed in the cycle-LTL logic. |
| first_indexed | 2024-04-10T02:24:09Z |
| format | Article |
| id | doaj.art-81e74bef07b44382b905e9e27aae2dde |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2025-03-14T08:52:02Z |
| publishDate | 2020-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-81e74bef07b44382b905e9e27aae2dde2025-03-02T12:46:59ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172020-12-0127441242710.18255/1818-1015-2020-4-412-4271089Temporal Logic for Programmable Logic ControllersNatalia Olegovna Garanina0Igor Sergeevich Anureev1Vladimir Evgenyevich Zyubin2Sergey Mikhailovich Staroletov3Tatiana Victorovna Liakh4Andrey Sergeevich Rozov5Sergei Petrovich Gorlatch6A.P. Ershov Institute of Informatics Systems (IIS), Siberian Branch of the Russian Academy of SciencesA.P. Ershov Institute of Informatics Systems (IIS), Siberian Branch of the Russian Academy of SciencesInstitute of Automation and Electrometry SB RASPolzunov Altai State Technical UniversityInstitute of Automation and Electrometry SB RASInstitute of Automation and Electrometry SB RASUniversity of MunsterWe address the formal verification of the control software of critical systems, i.e., ensuring the absence of design errors in a system with respect to requirements. Control systems are usually based on industrial controllers, also known as Programmable Logic Controllers (PLCs). A specific feature of a PLC is a scan cycle: 1) the inputs are read, 2) the PLC states change, and 3) the outputs are written. Therefore, in order to formally verify PLC, e.g., by model checking, it is necessary to describe the transition system taking into account this specificity and reason both in terms of state transitions within a cycle and in terms of larger state transitions according to the scan-cyclic semantics. We propose a formal PLC model as a hyperprocess transition system and temporal cycle-LTL logic based on LTL logic for formulating PLC property. A feature of the cycle-LTL logic is the possibility of viewing the scan cycle in two ways: as the effect of the environment (in particular, the control object) on the control system and as the effect of the control system on the environment. For both cases we introduce modified LTL temporal operators. We also define special modified LTL temporal operators to specify inside properties of scan cycles. We describe the translation of formulas of cycle-LTL into formulas of LTL, and prove its correctness. This implies the possibility ofmodel checking requirements expressed in logic cycle-LTL, by using well-known model checking tools with LTL as specification logic, e.g., Spin. We give the illustrative examples of requirements expressed in the cycle-LTL logic.https://www.mais-journal.ru/jour/article/view/1433formal verificationtemporal logicstransition systemsprogrammable logic controllers (plc) |
| spellingShingle | Natalia Olegovna Garanina Igor Sergeevich Anureev Vladimir Evgenyevich Zyubin Sergey Mikhailovich Staroletov Tatiana Victorovna Liakh Andrey Sergeevich Rozov Sergei Petrovich Gorlatch Temporal Logic for Programmable Logic Controllers Моделирование и анализ информационных систем formal verification temporal logics transition systems programmable logic controllers (plc) |
| title | Temporal Logic for Programmable Logic Controllers |
| title_full | Temporal Logic for Programmable Logic Controllers |
| title_fullStr | Temporal Logic for Programmable Logic Controllers |
| title_full_unstemmed | Temporal Logic for Programmable Logic Controllers |
| title_short | Temporal Logic for Programmable Logic Controllers |
| title_sort | temporal logic for programmable logic controllers |
| topic | formal verification temporal logics transition systems programmable logic controllers (plc) |
| url | https://www.mais-journal.ru/jour/article/view/1433 |
| work_keys_str_mv | AT nataliaolegovnagaranina temporallogicforprogrammablelogiccontrollers AT igorsergeevichanureev temporallogicforprogrammablelogiccontrollers AT vladimirevgenyevichzyubin temporallogicforprogrammablelogiccontrollers AT sergeymikhailovichstaroletov temporallogicforprogrammablelogiccontrollers AT tatianavictorovnaliakh temporallogicforprogrammablelogiccontrollers AT andreysergeevichrozov temporallogicforprogrammablelogiccontrollers AT sergeipetrovichgorlatch temporallogicforprogrammablelogiccontrollers |