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

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