A User-Friendly Verification Approach for IEC 61131-3 PLC Programs
Programmable logic controllers (PLCs) are special embedded computers that are widely used in industrial control systems. To ensure the safety of industrial control systems, it is necessary to verify the correctness of PLCs. Formal verification is considered to be an effective method to verify whethe...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2020-03-01
|
| Series: | Electronics |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2079-9292/9/4/572 |
| _version_ | 1797626438329827328 |
|---|---|
| author | Jiawen Xiong Gang Zhu Yanhong Huang Jianqi Shi |
| author_facet | Jiawen Xiong Gang Zhu Yanhong Huang Jianqi Shi |
| author_sort | Jiawen Xiong |
| collection | DOAJ |
| description | Programmable logic controllers (PLCs) are special embedded computers that are widely used in industrial control systems. To ensure the safety of industrial control systems, it is necessary to verify the correctness of PLCs. Formal verification is considered to be an effective method to verify whether a PLC program conforms to its specifications, but the expertise requirements and the complexity make it hard to be mastered and widely applied. In this paper, we present a specification-mining-based verification approach for IEC 61131-3 PLC programs. It only requires users to review specifications mined from the program behaviors instead of model checking for specified specifications, which can greatly improve the efficiency of safety verification and is much easier for control system engineers to use. Moreover, we implement a proof-of-concept tool named PLCInspector that supports directly mining LTL specifications and data invariants from PLC programs. Two examples and one real-life case study are presented to illustrate its practicability and efficiency. In addition, a comparison with the existing verification approaches for PLC programs is discussed. |
| first_indexed | 2024-03-11T10:10:23Z |
| format | Article |
| id | doaj.art-f018f4fff6ec480d8d2156b78c1e8cba |
| institution | Directory Open Access Journal |
| issn | 2079-9292 |
| language | English |
| last_indexed | 2024-03-11T10:10:23Z |
| publishDate | 2020-03-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Electronics |
| spelling | doaj.art-f018f4fff6ec480d8d2156b78c1e8cba2023-11-16T14:33:54ZengMDPI AGElectronics2079-92922020-03-019457210.3390/electronics9040572A User-Friendly Verification Approach for IEC 61131-3 PLC ProgramsJiawen Xiong0Gang Zhu1Yanhong Huang2Jianqi Shi3National Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai 200062, ChinaNational Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai 200062, ChinaNational Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai 200062, ChinaNational Trusted Embedded Software Engineering Technology Research Center, East China Normal University, Shanghai 200062, ChinaProgrammable logic controllers (PLCs) are special embedded computers that are widely used in industrial control systems. To ensure the safety of industrial control systems, it is necessary to verify the correctness of PLCs. Formal verification is considered to be an effective method to verify whether a PLC program conforms to its specifications, but the expertise requirements and the complexity make it hard to be mastered and widely applied. In this paper, we present a specification-mining-based verification approach for IEC 61131-3 PLC programs. It only requires users to review specifications mined from the program behaviors instead of model checking for specified specifications, which can greatly improve the efficiency of safety verification and is much easier for control system engineers to use. Moreover, we implement a proof-of-concept tool named PLCInspector that supports directly mining LTL specifications and data invariants from PLC programs. Two examples and one real-life case study are presented to illustrate its practicability and efficiency. In addition, a comparison with the existing verification approaches for PLC programs is discussed.https://www.mdpi.com/2079-9292/9/4/572IEC 61131-3 standardindustrial control systemPLCspecification miningverification |
| spellingShingle | Jiawen Xiong Gang Zhu Yanhong Huang Jianqi Shi A User-Friendly Verification Approach for IEC 61131-3 PLC Programs Electronics IEC 61131-3 standard industrial control system PLC specification mining verification |
| title | A User-Friendly Verification Approach for IEC 61131-3 PLC Programs |
| title_full | A User-Friendly Verification Approach for IEC 61131-3 PLC Programs |
| title_fullStr | A User-Friendly Verification Approach for IEC 61131-3 PLC Programs |
| title_full_unstemmed | A User-Friendly Verification Approach for IEC 61131-3 PLC Programs |
| title_short | A User-Friendly Verification Approach for IEC 61131-3 PLC Programs |
| title_sort | user friendly verification approach for iec 61131 3 plc programs |
| topic | IEC 61131-3 standard industrial control system PLC specification mining verification |
| url | https://www.mdpi.com/2079-9292/9/4/572 |
| work_keys_str_mv | AT jiawenxiong auserfriendlyverificationapproachforiec611313plcprograms AT gangzhu auserfriendlyverificationapproachforiec611313plcprograms AT yanhonghuang auserfriendlyverificationapproachforiec611313plcprograms AT jianqishi auserfriendlyverificationapproachforiec611313plcprograms AT jiawenxiong userfriendlyverificationapproachforiec611313plcprograms AT gangzhu userfriendlyverificationapproachforiec611313plcprograms AT yanhonghuang userfriendlyverificationapproachforiec611313plcprograms AT jianqishi userfriendlyverificationapproachforiec611313plcprograms |