TY - GEN
T1 - Cooperative Verification of PLC Programs Using CoVeriTeam
T2 - 2023 Cyber-Physical Systems and Internet-of-Things Week, CPS-IoT Week 2023
AU - Ukegbu, Chibuzo
AU - Mehrpouyan, Hoda
N1 - Publisher Copyright:
© 2023 ACM.
PY - 2023/5/9
Y1 - 2023/5/9
N2 - It is important that the programmed logic controller(PLC), the heart of industrial control systems (ICS), is formally verified to ensure that its safety and security requirements are met. However, the combination of the strengths of two or more verification tools to verify tasks has yet to be fully explored, especially in verification of safety-critical programs such as PLC programs. In this paper, we apply cooperative verification techniques by building a verifier validator (using Symbiotic as a verifier and the CPA checker as a validator). We investigate the possibilities of preventing false positives in verification results and discover how effective and efficient the (verifier-validator) is when compared with a single verification tool. The results show that the verifier validator was able to discover 3 properties that were not properly verified by a single verification tool in a shorter time span.
AB - It is important that the programmed logic controller(PLC), the heart of industrial control systems (ICS), is formally verified to ensure that its safety and security requirements are met. However, the combination of the strengths of two or more verification tools to verify tasks has yet to be fully explored, especially in verification of safety-critical programs such as PLC programs. In this paper, we apply cooperative verification techniques by building a verifier validator (using Symbiotic as a verifier and the CPA checker as a validator). We investigate the possibilities of preventing false positives in verification results and discover how effective and efficient the (verifier-validator) is when compared with a single verification tool. The results show that the verifier validator was able to discover 3 properties that were not properly verified by a single verification tool in a shorter time span.
KW - Control Logic
KW - Cooperative verification
KW - Formal verification
UR - http://www.scopus.com/inward/record.url?scp=85159785583&partnerID=8YFLogxK
U2 - 10.1145/3576914.3587490
DO - 10.1145/3576914.3587490
M3 - Conference contribution
AN - SCOPUS:85159785583
T3 - ACM International Conference Proceeding Series
SP - 37
EP - 42
BT - Proceedings of 2023 Cyber-Physical Systems and Internet-of-Things Week, CPS-IoT Week 2023 - Workshops
Y2 - 9 May 2023 through 12 May 2023
ER -