ESBMC-PLC+: PLCverif의 후속작으로서 통합된 IEC 61131-3 형식 검증 프레임워크

PLCverif는 CERN에서 개발되어 2019년부터 실무에 사용되고 있는 PLC 형식 검증 (formal verification) 분야에서 가장 성숙한 오픈 소스 플랫폼입니다. 하지만 여기에는 두 가지 근본적인 한계가 있습니다. 첫째, 지배적인 PLC 표기법인 래더 다이어그램 (Ladder Diagram, LD) 프로그램을 지원하지 않는다는 점이며, 둘째는 주요 백엔드 (backend)로 CBMC에 의존하고 있어 검증이 유계 증명 (bounded proofs)으로 제한된다는 점입니다. PLCverif의 저자들 스스로도 ESBMC를 적절한 백엔드 개선안으로 식별했습니다. 이전 연구에서는 ESBMC-PLC (k-유도 (k-induction)를 포함한 텍스트 기반 LD 프런트엔드)와 ESBMC-GraphPLC (그래픽 기반 PLCopen XML 지원)를 구축했습니다. 이들은 함께 유계가 없는 증명 (unbounded proofs)을 통한 LD를 지원하지만, 구조화된 텍스트 (Structured Text, ST)는 지원하지 않으며, 타이머/카운터 기능 블록 (function blocks)을 포함한 그래픽 LD는 여전히 검증이 불가능한 상태로 남아 있습니다.

본 논문은 이러한 두 가지 간극을 모두 메우는 통합 프레임워크인 ESBMC-PLC+를 제시합니다: (1) MATIEC IEC 61131-3 컴파일러를 통한 ST/SCL 프런트엔드 구현으로, C로 컴파일된 ST를 비결정론적 입력 모델링 (nondeterministic input modeling) 및 YAML 속성 주입 (property injection)과 함께 ESBMC로 전달합니다. (2) 그래픽 LD를 위한 기능 블록 상태 의미론 (function block state semantics)을 도입하여, DFS 리졸버 (DFS resolver)를 확장함으로써 TON/TOF/TP 타이머, CTU/CTD 카운터, 그리고 R_TRIG/F_TRIG 에지 트리거 (edge triggers)를 GOTO IR 내의 지속적인 스캔 사이클 상태 변수로 모델링합니다.

ESBMC-PLC+는 단일 ESBMC 백엔드를 통해 세 가지 주요 IEC 61131-3 입력 형식을 모두 지원하며, k-유도 기반의 유계가 없는 안전성 증명 (unbounded safety proofs)을 가능하게 하는 최초의 오픈 소스 PLC 검증 프레임워크입니다. PLCverif와의 기능 비교 및 최대 8개의 정수 타이머를 포함한 8개의 벤치마크 프로그램에 대한 실험적 평가 결과, ESBMC-PLC+는 PLCverif의 입력 커버리지를 충족하면서도 더 강력한 보증을 제공함을 보여줍니다. nuXmv의 BDD 백엔드와 비교했을 때, ESBMC-PLC+는 타이머 프로그램에서 400~2,000배 더 빠르며, nuXmv BDD가 120초에서 타임아웃되는 증명들을 완료해냅니다.