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

Chibuzo Ukegbu, Hoda Mehrpouyan

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationICISE 2023 - 8th International Conference on Information Systems Engineering
Pages19-28
Number of pages10
ISBN (Electronic)9798400709173
DOIs
StatePublished - 16 Dec 2023
Event8th International Conference on Information Systems Engineering, ICISE 2023 - Bangkok, Thailand
Duration: 16 Dec 202318 Dec 2023

Publication series

NameACM International Conference Proceeding Series

Conference

Conference8th International Conference on Information Systems Engineering, ICISE 2023
Country/TerritoryThailand
CityBangkok
Period16/12/2318/12/23

Keywords

  • Benchmark
  • CoVeriTeam
  • PLC
  • safety and security properties
  • Verification

Fingerprint

Dive into the research topics of 'Benchmarks for the Verification of Safety and Security Properties of PLC Programs in Cooperative Verification Environments'. Together they form a unique fingerprint.

Cite this