Benchmarks for the Verification of Safety and Security Properties of PLC Programs in Cooperative Verification Environments

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.