TY - GEN
T1 - Benchmarks for the Verification of Safety and Security Properties of PLC Programs in Cooperative Verification Environments
AU - Ukegbu, Chibuzo
AU - Mehrpouyan, Hoda
N1 - Publisher Copyright:
© 2023 Owner/Author.
PY - 2023/12/16
Y1 - 2023/12/16
N2 - Cooperative verification is a promising technique for verifying the safety and security properties of Programmable Logic Controllers (PLCs). However, cooperative verification has not yet been widely used for PLC programs, and there are no cooperative verification benchmarks for PLC programs. This paper presents verification tools and property benchmarks for cooperative verification of the safety and security properties of PLC programs. We developed two algorithms: 1) to select and rank verification tools that satisfy the tool selection requirement of PLC programs. 2) A verifier validator that cooperatively verifies PLC programs using three complementary verification tools. We added a property benchmark that adds the end-of-the-cycle (EoC) variable to the LTL specification property to adjust the tool's verification from step semantics to the PLC's scan-cycle semantics. We conducted experiments using CoVeriTeam(a cooperative verification framework) with 40 real-world PLC programs from PLCOpen. Our approach significantly enhances the accuracy and reliability of PLC program verification by recommending tools that our experiments show to have the lowest false positive rate (FPR) and false negative rates(FNR). We recommend CBMC, CPA-SEQ, and Symbiotic as the go-to tools for cooperative verification of PLC programs using CoVeriTeam.
AB - Cooperative verification is a promising technique for verifying the safety and security properties of Programmable Logic Controllers (PLCs). However, cooperative verification has not yet been widely used for PLC programs, and there are no cooperative verification benchmarks for PLC programs. This paper presents verification tools and property benchmarks for cooperative verification of the safety and security properties of PLC programs. We developed two algorithms: 1) to select and rank verification tools that satisfy the tool selection requirement of PLC programs. 2) A verifier validator that cooperatively verifies PLC programs using three complementary verification tools. We added a property benchmark that adds the end-of-the-cycle (EoC) variable to the LTL specification property to adjust the tool's verification from step semantics to the PLC's scan-cycle semantics. We conducted experiments using CoVeriTeam(a cooperative verification framework) with 40 real-world PLC programs from PLCOpen. Our approach significantly enhances the accuracy and reliability of PLC program verification by recommending tools that our experiments show to have the lowest false positive rate (FPR) and false negative rates(FNR). We recommend CBMC, CPA-SEQ, and Symbiotic as the go-to tools for cooperative verification of PLC programs using CoVeriTeam.
KW - Benchmark
KW - CoVeriTeam
KW - PLC
KW - safety and security properties
KW - Verification
UR - http://www.scopus.com/inward/record.url?scp=85196429620&partnerID=8YFLogxK
U2 - 10.1145/3641032.3641046
DO - 10.1145/3641032.3641046
M3 - Conference contribution
AN - SCOPUS:85196429620
T3 - ACM International Conference Proceeding Series
SP - 19
EP - 28
BT - ICISE 2023 - 8th International Conference on Information Systems Engineering
T2 - 8th International Conference on Information Systems Engineering, ICISE 2023
Y2 - 16 December 2023 through 18 December 2023
ER -