ESBMC-GraphPLC: SMT 기반 모델 체킹을 이용한 그래픽 PLCopen XML 래더 다이어그램 프로그램의 형식 검증

PLCopen XML은 IEC 61131-3 래더 다이어그램 (Ladder Diagram, LD) 프로그램을 위한 두 가지 인코딩 형식을 정의합니다. 하나는 <rung> 요소를 사용하는 텍스트 인코딩이며, 다른 하나는 rung 로직을 localId/refLocalId 연결의 유향 그래프 (directed graph)로 표현하는 그래픽 인코딩입니다. ESBMC-PLC는 텍스트 형식을 지원했으나, CONTROLLINO, Beremiz, OpenPLC Editor에서 내보낸 그래픽 파일을 빈 GOTO 중간 표현 (intermediate representation, IR)으로 파싱하여, 실질적인 검증 없이 성공하는 공허한 검증 (vacuous verification) 문제를 일으켰습니다. 본 논문은 DFS 기반의 그래픽 LD 리졸버 (resolver)를 통해 이 격차를 해소하는 ESBMC-GraphPLC를 제시합니다. 이 리졸버는 leftPowerRail에서 각 코일 (coil)까지의 연결 그래프를 탐색하고, rung 경로를 불리언 접점 결합 (Boolean contact conjunctions)으로 추출하며, 3단계 I/O 추론 체계를 적용합니다. rightPowerRail connectionPointIn 순서에 따라 코일을 정렬함으로써 SET 코일이 RESET 코일보다 먼저 처리되도록 하여, IEC 스캔 사이클 (scan-cycle) 의미론과 일치시킵니다. 그래픽-to-IR 변환은 ESBMC 백엔드를 변경하지 않습니다. CONTROLLINO/OpenPLC Editor에서 가져온 3개의 그래픽 LD 프로그램에 대한 검증 결과, 이전의 빈 IR과 달리 비결정론적 입력 (nondeterministic inputs) 및 rung 로직을 포함한 완전한 GOTO IR이 생성됨을 보여줍니다. 3개 프로그램 모두 k=2에서 70ms 이내에 SAFE 상태임을 검증했습니다. 11개의 텍스트 LD 벤치마크는 회귀(regression) 없이 완전히 보존되었습니다. LD 콘텐츠가 없거나 지원되지 않는 타이머 의미론을 가진 두 개의 Beremiz 예시는 발견된 한계점으로 보고되었습니다. Artifact는 Zenodo (DantasCordeiro2026graphical, doi:10.5281/zenodo.20699856)에서 확인할 수 있습니다.