ESBMC-PLC: SMT 기반 모델 체킹을 이용한 IEC 61131-3 래더 다이어그램 프로그램의 형식 검증

PLC(Programmable Logic Controllers)는 산업 전반에 걸쳐 안전에 직결되는 프로그램을 실행합니다. IEC 61131-3 표준에 따른 지배적인 PLC 표기법인 래더 다이어그램 (Ladder Diagram, LD)은 여전히 형식 검증 (Formal Verification) 대상에서 제외되어 있습니다. SMT 기반 모델 체커 (SMT-based model checkers)가 LD의 렁(rung) 및 코일(coil) 그래픽을 처리할 수 없기 때문입니다. 본 논문은 새로운 ESBMC 프론트엔드로 구현되어, 네이티브 LD 지원 (PLCopen XML 형식)을 갖춘 최초의 오픈 소스 형식 검증기인 ESBMC-PLC를 제시합니다. ESBMC-PLC는 LD 렁을 GOTO IR로 변환하고, PLC 스캔 사이클을 비결정론적 입력 (nondeterministic inputs)을 가진 while(true) 루프로 모델링하며, SMT 기반 유계 모델 체킹 (Bounded Model Checking) 또는 k-유도 (k-induction)를 통해 안전 속성 (Safety Properties)을 확인합니다. 5가지 속성 YAML 언어 (mutual_exclusion, invariant, absence, response, reachability)를 사용하여 시계열 논리 (Temporal Logic)를 피했습니다. 22개의 연구 (2020-2026)에 대한 조사 결과 4가지 연구 공백이 확인되었으며, ESBMC-PLC는 그중 2개를 해결합니다. 13개의 벤치마크 (6개 도메인, 실제 배포된 CONTROLLINO PLC 및 MathWorks Simulink PLC Coder를 포함한 3개 소스)에 대한 평가 결과, 61개 속성에 대해 정확한 분류를 보여주었습니다: 저자가 작성한 9개 프로그램 모두 (카테고리 A/B) 예상대로 작동하였고, 4개의 벤더 프로그램 (카테고리 C)은 레이블 없이 올바르게 분류되었으며, 8개의 버그를 발견하였고 (실행 가능한 반례 제공), 7개의 유계되지 않은 k-유도 증명을 수행하였으며, 모든 실행은 Apple Silicon에서 60ms 미만으로 완료되었습니다. PLCverif와의 기능 비교를 통해, ESBMC-PLC가 네이티브 LD, k-유도, 그리고 SMT 비트 벡터 의미론 (Bit-vector Semantics)을 결합한 유일한 오픈 소스 도구임을 입증했습니다.