💬 NLP

ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking

이 논문은 그래프 기반의 래더 다이어그램(Ladder Diagram)을 처리하는 데 발생하는 공백을 해결하기 위해, 그래프 기반 렁(rung) 로직을 SMT 기반 모델 체킹을 위한 유효한 GOTO 중간 표현으로 변환하는 DFS 기반 리졸버를 구현함으로써, 기존의 텍스트 형식 지원에 영향을 주지 않으면서 CONTROLLINO 및 OpenPLC Editor와 같은 에디터로부터 생성된 프로그램을 정확하게 검증할 수 있게 하는 정형 검증 도구인 ESBMC-GraphPLC를 소개한다.

원저자: Pierre Dantas, Lucas Cordeiro, Waldir Junior

게시일 2026-06-19

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Pierre Dantas, Lucas Cordeiro, Waldir Junior

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

**프로그래머블 로직 컨트롤러(PLC)**를 워터 펌프나 신호등 같은 공장 기계의 두뇌라고 상상해 보세요. 이 두뇌에 무엇을 할지 알려주기 위해 엔지니어들은 **래더 다이어그램(Ladder Diagrams)**을 그립니다. 이것은 마치 사다리의 가로대(rung)가 있는 전기 사다리처럼 보이며, 각 가로대는 하나의 규칙이 됩니다: "만약 물탱크가 가득 차면, 펌프를 꺼라."

오랫동안 컴퓨터에 이러한 래더 그림을 저장하는 데는 두 가지 방법이 있었습니다:

텍스트 리스트(The Text List): 단순하고 단계적인 명령 목록 (마치 레시피와 같습니다).
그래픽 맵(The Graphical Map): 구성 요소들이 ID 번호로 식별된 보이지 않는 전선들로 연결된 시각적 지도 (마치 역들이 선으로 연결된 지하철 노선도와 같습니다).

문제점: "유령" 프로그램

연구진은 이 프로그램들의 안전 오류를 점검할 수 있는 ESBMC-PLC라는 강력한 도구를 가지고 있었습니다. 이 도구는 텍스트 리스트 형식에서는 완벽하게 작동했습니다.

하지만 연구진이 현대적인 소프트웨어인 CONTROLLINO나 OpenPLC에서 실제로 사용하는 그래픽 맵 형식을 입력했을 때, 도구는 혼란에 빠졌습니다. 도구는 지도를 보고 ID 번호와 전선을 보았지만, 그것들이 어떻게 연결되어 있는지 파악하지 못했습니다.

결과: 도구는 "모든 것이 안전하다!"라고 말했습니다.
함정: 그것은 거짓말이었습니다. 논리가 누락되었기 때문에 "안전"한 것이 아니라, 도구가 빈 방을 보고 있었기 때문입니다. 이것을 **공허한 검증(vacuous verification)**이라고 합니다. 이는 마치 문이 잠겨 있는지 확인하기 위해 창문이 열려 있는지 체크하는 것을 잊어버린 채, 문이 잠겨 있으니 안전하다고 말하는 것과 같습니다.

해결책: ESBMC-GraphPLC

저자들은 이를 해결하기 위해 ESBMC-GraphPLC라는 새로운 모듈을 구축했습니다. 이것을 그래픽 맵을 돌아다니며 안전 점검 도구가 이해할 수 있는 언어로 다시 번역하는 탐정을 고용하는 것이라고 생각하면 됩니다.

이 "탐정"이 어떻게 작동하는지 쉬운 비유를 통해 설명하겠습니다:

1. 손전등을 든 탐정 (DFS 알고리즘)
이 도구는 **깊이 우선 탐색(Depth-First Search, DFS)**이라는 방법을 사용합니다. 탐정이 전선 미로를 헤매는 모습을 상상해 보세요. 그들은 사다리의 왼쪽(전원 공급원)에서 시작하여 오른쪽까지 가능한 모든 경로를 따라갑니다.

모든 전선 연결을 추적합니다.
지나가는 모든 스위치(접점)를 기록합니다.
장치(코일/펌프)에 도달하면 멈춥니다.
이렇게 함으로써, 시각적 지도를 다시 명확한 "If-Then" 규칙으로 재구성하여 래더의 정확한 논리를 복원합니다.

2. 교통 경찰 (순서의 중요성)
이 다이어그램에서는 가끔 동일한 장치에 대해 "Set" 스위치(켜기)와 "Reset" 스위치(끄기)가 함께 존재합니다. 이때는 순서가 중요합니다!

만약 같은 찰나에 "Set"이 "Reset"보다 먼저 일어난다면, 장치는 켜진 상태를 유지합니다.
만약 "Set"이 "Reset" 이후에 일어난다면, 장치는 꺼진 상태가 됩니다.
새로운 도구는 파일의 특정 목록(rightPowerRail 시퀀스)을 살펴보고 어떤 스위치가 먼저 오는지 확인하여, "Set" 자동차가 "Reset" 자동차보다 먼저 가도록 하는 교통 경찰처럼 작동합니다. 이를 통해 실제 기계가 실제로 동작하는 방식과 일로직을 일치시킵니다.

3. 추측 게임 (I/O 추론)
때때로 지도는 어떤 전선이 "입력(센서)"이고 어떤 전선이 "출력(모터)"인지 명시하지 않습니다. 도구는 세 단계의 추측 게임을 사용합니다:

1단계: 공식 주소 라벨(예: 입력을 나타내는 %IX)을 찾습니다. 라벨이 있다면 정확합니다.
2단계: 라벨이 없다면, 동작을 관찰합니다. 만약 어떤 전선이 오직 스위치로만 사용된다면, 그것은 아마도 입력일 것입니다. 만약 어떤 전선이 오직 무언가를 켜는 데만 사용된다면, 그것은 아마도 출력일 것입니다.
3단계: 여전히 확실하지 않다면, 그것을 무엇이든 될 수 있는 "미지의 변수"로 취급합니다. 이는 모든 가능성을 점검하여 놓치는 것이 없도록 하는 안전한 선택입니다.

결과

팀은 이 새로운 탐정을 세 가지 실제 프로그램(워터 펌프, 계단 조명, 디머 조명)에 테스트했습니다.

이전: 도구는 빈 방을 보고 "안전"하다고 잘못 말했습니다.
이후: 도구는 전체 논리를 파악했고, 가능한 모든 센서 입력의 조합을 점검했으며, 프로그램이 실제로 안전함을 확인했습니다.
속도: 이 과정은 70밀리초 미만(사람의 눈 깜빡임보다 빠름)에 완료되었습니다.
안전성: 기존 도구를 망가뜨리지 않았습니다. 텍스트 리스트로 이미 잘 작동하던 11개의 프로그램도 완벽하게 작동했습니다.

아직 할 수 없는 것 (한계점)

논문은 이 탐정이 여전히 어려움을 겪고 있는 부분에 대해 솔직하게 밝히고 있습니다:

복잡한 타이머: 만약 래더에 타이머(예: "5초를 기다린 후 켜라")가 포함되어 있다면, 현재 도구는 "기다림" 부분을 무시하고 이를 무작위 추측으로 처리합니다. 안전하긴 하지만, 타이밍을 이해하지는 못합니다.
중첩된 맵(Nested Maps): 일부 복잡한 다이어그램은 다른 섹션 안에 더 작은 맵을 숨겨 놓습니다(예: 단계 내부의 동작). 탐정은 가끔 이러한 숨겨진 방을 놓치기도 합니다.

요약

요약하자면, 저자들은 안전 점검 소프트웨어가 현대 산업용 소프트웨어에서 사용하는 시각적 래더 다이어그램을 마침내 "읽을 수 있도록" 해주는 번역기를 만들었습니다. 그들은 단순히 "모든 것이 괜찮다"라고 맹목적으로 말하던 도구를, 논리를 실제로 이해하고 기계가 고장 나거나 사람을 다치게 하지 않을 것임을 증명할 수 있는 도구로 바꾸어 놓았습니다.

기술 요약: ESBMC-GraphPLC

문제 정의
본 논문은 ESBMC-PLC 도구를 이용한 프로그래머블 로직 컨트롤러(PLC) 프로그램의 형식 검증에서 발생하는 결정적인 공백 문제를 다룹니다. ESBMC-PLC는 PLCopen XML(tc6_0201)의 텍스트 형식은 성공적으로 지원했지만, CONTROLLINO, Beremiz, OpenPLC Editor와 같은 주요 개발 환경의 기본 내보내기 형식인 **그래픽 형식(graphical format)**을 올바르게 처리하는 데 실패했습니다.

그래픽 형식에서 래더 다이어그램(LD) 로직은 명시적인 <rung> 요소가 아닌 localId 및 refLocalId 연결로 구성된 유향 그래프(directed graph)로 인코딩됩니다. 기존 파서는 이러한 파일들을 감지했으나 렁(rung)을 찾지 못해 빈 GOTO 중간 표현(IR)을 생성했습니다. 결과적으로 모든 변수가 0으로 초기화되었으며, 이는 속성이 공허하게(vacuously) 성립되는 결과를 초래했습니다. 즉, 로직이 전혀 생성되지 않았기 때문에 속성이 사소하게 만족된 것이며, 이는 PLC 로직의 안전성을 실제로 보장하지 못했습니다.

방법론
저자들은 그래픽 연결 그래프로부터 렁 로직을 재구성하기 위해 깊이 우선 탐색(DFS) 기반의 리졸버(resolver)를 구현함으로써 이 간극을 메우는 ESBMC-GraphPLC 모듈을 제안합니다. 이 방법론은 세 가지 핵심 구성 요소를 포함합니다:

그래픽 LD 리졸버 및 렁 추출:
- 시스템은 localId/refLocalId 그래프를 파싱하여 leftPowerRail에서 각 코일(coil)까지의 경로를 식별합니다.
- 그래프를 순회하여 접점(contact) 시퀀스를 추출하고, 이를 불리언 논리곱(Boolean conjunctions)으로 변환합니다.
- 결정적 순서 통찰: IEC 61131-3 스캔 사이클 의미론을 준수하기 위해, 알고리즘은 rightPowerRail의 connectionPointIn 리스트에 있는 refLocalId 항목의 순서에 따라 코일 처리 순서를 결정합니다. 이를 통해 동일한 스캔 사이클 내에서 SET 코일이 RESET 코일보다 먼저 처리되도록 하여 올-바른 래치(latch) 동작을 보존합니다.
3단계 I/O 추론:
입력(비결정적 재샘플링)과 출력(지속적 상태)을 올바르게 모델링하기 위해, 도구는 계층적 분류 체계를 사용합니다:
- 1단계: 명시적인 IEC 61131-3 하드웨어 주소(%IX는 입력, %QX는 출력)를 사용합니다.
- 2단계: 주소가 없는 프로그램을 위한 휴리스틱 분석을 적용하여, 접점으로만 나타나는 변수는 입력으로, 코일로만 나타나는 변수는 출력으로 분류합니다.
- 3단계: 분류되지 않은 변수는 내부 지속 상태(internal persistent state)로 취급합니다.
구현 전략:
이 솔루션은 프론트엔드 파서(plcopen_xml_parser.cpp, +274행) 내에서 완전히 구현되었습니다. GOTO IR 인코더, k-유도 엔진, Z3 SMT 솔버 또는 속성 인코더를 포함한 ESBMC 백엔드의 변경은 전혀 필요하지 않습니다. 리졸버는 텍스트 파서가 생성하는 구조와 동일한 표준 RungNode 리스트를 출력합니다.

주요 기여

형식 모델: 그래픽 LD 연결 그래프에 대한 형식적 정의와, DFS로 추출된 경로가 IEC 61131-3 스캔 사이클 의미론과 동등함을 증명하는 건전성(soundness) 정리를 제시합니다.
알고리즘 솔루션: SET/RESET 순서를 올바르게 처리하는 그래픽 PLCopen XML용 DFS 기반 렁 추출기의 최초 오픈 소스 구현입니다.
하위 호환성: 이 확장은 기존의 텍스트 LD 벤치마크에 대한 모든 기능을 유지하며 회귀(regression)가 없습니다.
산출물: 도구, 벤치마크, 검증을 위한 Python 프로토타입을 포함한 완전하고 재현 가능한 산출물을 제공합니다.

실험 결과
도구는 CONTROLLINO 및 OpenPLC Editor에서 내보낸 3개의 그래픽 LD 프로그램에 대해 평가되었습니다:

물 제어 (water_control): 5개 렁 (2 SET, 3 RESET).
계단 조명 (stairs_light): 6개 렁 (2 SET, 2 RESET, 2 일반).
디머 조명 (dimmer_light_control): 4개 렁 (일반).

결과:

IR 완결성: 3개 프로그램 모두 "빈 IR"(공허함) 상태에서 비결정적 입력과 전체 렁 로직을 포함하는 "전체 IR" 상태로 전환되었습니다.
검증: 3개 프로그램 모두 $k=2$ 에서 70ms 미만으로 SAFE임을 검증했습니다 (중앙값 시간: 50ms, 40ms, 60ms).
회귀 테스트: 11개의 실제 텍스트 LD 벤치마크는 동일한 결과를 생성하여, 제로 회귀를 확인했습니다.

한계 및 범위
본 논문은 현재의 리졸버가 렁 경로 내에서 펑션 블록(타이머, 카운터, 비교기)의 의미론을 보존하지 못한다고 명시적으로 언급합니다. 만약 렁이 펑션 블록에 의존하는 경우, 도구는 해당 블록의 출력을 비결정적 항(nondeterministic term)으로 취급하거나(건전한 과대 근사), beremiz_traffic_light 예시와 같은 특정 사례에서는 로직이 상수로 붕괴됩니다. 타이밍 의미론이 손실된 프로그램에 대해 오해의 소지가 있는 "SAFE" 판정을 보고하는 것을 피하기 위해 두 개의 Beremiz 예시는 결과에서 제외되었습니다.

의의
본 논문은 ESBMC-GraphPLC가 현대적 PLC 개발 환경의 표준 출력인 그래픽 PLCopen XML 프로그램의 건전하고 공허하지 않은 형식 검증을 가능하게 한다고 주장합니다. 그래픽 내보내기와 SMT 기반 모델 체킹 사이의 간극을 메움으로써, 자동화 엔지니어들이 수동으로 텍스트 형식으로 변환하지 않고도 안전 속성(예: 펌프 제어, 신호등)을 검증할 수 있게 합니다. 저자들은 현재 구현이 접점/코일 네트워크와 SET/RESET 래치를 효과적으로 처리하지만, 더 복잡한 순차 제어 로직을 지원하기 위해서는 펑션 블록 의미론을 통합하는 후속 연구가 필요함을 강조합니다.

문제점: "유령" 프로그램

해결책: ESBMC-GraphPLC

결과

아직 할 수 없는 것 (한계점)

요약

기술 요약: ESBMC-GraphPLC

유사한 논문