💬 NLP

ESBMC-PLC: Formal Verification of IEC 61131-3 Ladder Diagram Programs Using SMT-Based Model Checking

이 논문은 IEC 61131-3 래더 다이어그램 프로그램을 SMT 기반 모델 체킹을 위한 중간 표현으로 변환함으로써 이를 네이티브하게 지원하는 최초의 오픈 소스 정형 검증기인 ESBMC-PLC를 소개하며, 이를 통해 해당 분야의 주요 연구 공백을 해결하는 동시에 다양한 산업 벤치마크에서 안전 속성을 성공적으로 검증하고 버그를 탐지한다.

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

게시일 2026-06-16

📖 3 분 읽기☕ 가벼운 읽기

CC BY 4.0

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

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

거대한 기계, 화학 혼합기, 열차 신호가 PLC(프로그래머블 로직 컨트롤러)라는 작고 지치지 않는 두뇌에 의해 제어되는 공장 바닥을 상상해 보십시오. 이 기계들은 래더 다이어그램(Ladder Diagram)이라는 특별한 종류의 명령어 매뉴얼을 바탕으로 작동합니다. 이것은 마치 사다리 그림과 같아서, 각 "가로대(rung)"는 하나의 규칙이 됩니다: "만약 빨간 불이 켜져 있고 버튼이 눌렸다면, 모터를 작동시켜라."

수십 년 동안 엔지니어들은 코드를 타이핑하는 대신 이 규칙들을 그림을 그려서 작성해 왔습니다. 이로 인해 현대적인 "안전 검사관"(형식 검증 도구)들이 이 규칙들이 완벽한지 확인하기가 매우 어려웠습니다. 왜냐하면 검사관들은 타이핑된 코드만 이해할 뿐, 그림은 이해하지 못했기 때문입니다.

이 논문은 ESBMC-PLC라는 새로운 도구를 소개합니다. 이 도구는 범용 번역기이자 매우 엄격한 안전 검사관의 역할을 동시에 수행합니다.

이 도구가 어떻게 작동하는지 쉬운 비유를 통해 설명하겠습니다.

1. 번역기 (The "Rosetta Stone")

이 도구가 나오기 전에는 컴퓨터에게 그림을 검사해달라고 요청할 수 없었습니다. ESBMC-PLC는 그래픽 형태의 "래더 다이어그램"(그림)을 가져와서 컴퓨터가 이해할 수 있는 언어(텍스트 기반 중간 코드)로 즉시 번역합니다.

비유: 여러분이 식재료 그림이 그려진 스케치북에 적힌 레시피를 가지고 있다고 상상해 보십시오. ESBMC-PLC는 그 그림을 보고 즉시 "밀가루 2컵을 넣고, 그다음 저으시오"와 같은 정확한 텍스트 명령어로 옮겨 적는 요리사와 같습니다. 이제 컴퓨터가 그 레시피를 읽을 수 있게 된 것입니다.

2. 시뮬레이터 (The "Time-Traveling Loop")

PLC는 단 한 번만 실행되는 것이 아니라, 센서를 확인하고 출력을 변경하며 끊임없이 루프(loop)를 돌며 작동합니다.

비유: 대부분의 안전 점검은 단 하나의 순간만을 살펴봅니다. 반면, ESBMC-PLC는 공장의 "하루"를 계속해서 반복해서 실행하는 시간 여행 시뮬레이터와 같습니다. 하지만 단순히 특정 하루를 다시 재생하는 것이 아니라, 모든 가능한 하루를 동시에 시뮬레이션합니다. "만약 센서가 고장 난다면? 만약 버튼이 두 번 눌린다면? 만약 전력이 깜빡거린다면?"이라고 질문하며, 재앙이 발생할 수 있는 모든 사건의 조합을 체크합니다.

3. "무한한" 증명 (The "Forever Guarantee")

기존의 도구들은 제한된 단계만을 확인할 수 있었습니다(예를 들어 공장의 첫 100일 동안만 확인하는 것). 만약 101일째 되는 날에 버그가 발생한다면, 기존 도구들은 이를 놓칠 수 있었습니다.

비유: ESBMC-PLC는 **k-유도(k-induction)**라고 불리는 특별한 수학적 기법을 사용합니다. 하루하루를 하나씩 세는 대신, "오늘 공장이 안전하고 규칙이 준수된다면, 내일도, 모레도, 그리고 영원히 안전할 것이다"라는 규칙을 증명합니다. 이는 기계가 규칙을 따르는 한 절대 충돌하지 않을 것이라는 영원한 보장을 제공합니다.

4. "논리 없는" 언어 (The "Plain English" Checklist)

보통 컴퓨터에게 안전성을 확인하도록 요청하려면 복잡한 수학적 논리(시제 논리)를 알아야 했습니다.

비유: ESBMC-PLC를 사용하면 엔지니어들이 간단한 YAML 체크리스트(할 일 목록과 같은 형태)로 안전 규칙을 작성할 수 있습니다.
- 기존 방식: "모든 시간 t에 대하여, A가 참이면 B는 반드시 거짓이어야 한다."
- 작성 방식: "모터와 역회전 스위치가 동시에 켜져서는 안 된다."
  이 도구는 이러한 평이한 영어 문장을 이해하고 자동으로 체크합니다.

무엇을 발견했는가?

저자들은 이 도구를 단순한 모터 제어부터 복잡한 신호등 및 워터 펌프에 이르기까지 13가지의 서로 다른 공장 프로그램에 테스트했습니다. 이 프로그램들은 도구의 성능을 시험하기 위해 설계된 것이 아니라, 실제 현장에서 쓰이는 제품(CONTROLLINO 및 MathWorks 등)에서 가져온 것들입니다.

결과:
- 100% 정확도: 안전한 프로그램과 안전하지 않은 프로그램을 모두 정확하게 식별해 냈습니다.
- 숨겨진 버그 발견: 표준 테스트가 놓쳤던 8가지의 구체적인 버그를 찾아냈습니다. 예를 들어, 비상 정지 버튼을 눌렀을 때 기계는 멈추지만 타이머가 리셋되지 않아, 버튼을 놓는 즉시 기계가 바로 재가동되는 시나리오를 찾아냈습니다.
- 속도: 이 모든 프로그램을 검사하는 데 60밀리초(ms) 미만이 걸렸습니다(사람이 눈을 깜빡이는 것보다 빠릅니다).

결론

이 논문은 표준 산업용 도면(래더 다이어그램)을 가져와 번역하고, 그것이 영원히 안전함을 수학적으로 증명할 수 있는 최초의 오픈 소스 도구를 제시합니다. 이는 엔지니어가 기계를 설계하는 전통적인 그래픽 방식과 컴퓨터가 안전성을 검증하는 첨단 수학 방식 사이의 간극을 메워줍니다.

중요 참고 사항: 이 논문은 이 도구가 산업용 프로그래밍의 특정 "핵심" 부분(불리언 논리, 타이머, 카운터)에 대해 작동한다고 명시합니다. 아직 부동 소수점 숫자나 고급 데이터 배열과 같은 복잡한 기능은 다루지 못하지만, 안전이 중요한 대부분의 로직에 대해서는 완벽하게 작동하며 지금 바로 사용할 준비가 되어 있습니다.

기술 요약: ESBMC-PLC

문제 정의

프로그래머블 로직 컨트롤러(PLC)는 산업 안전에 필수적이지만, IEC 61131-3 표준인 래더 다이어그램(Ladder Diagram, LD)은 현재 지배적인 프로그래밍 표기법임에도 불구하고 공식 검증 생태계에서 크게 결여되어 있다. ESBMC와 같은 SMT(Satisfiability Modulo Theories) 기반 모델 체커는 범용 소프트웨어(C, Rust, Python)를 위해 성숙해 왔으나, LD의 그래픽 기반 "rung-and-coil" 표기법을 직접 처리할 수는 없다. 기존 솔루션들은 수동 번역(텍스트 언어로 변환 시 충실도 위험 발생), 독점 도구 의존, 또는 무제한 안전 증명 지원 부족 등의 문제를 안고 있다. 결과적으로, 산업 제어 로직은 다른 소프트웨어 도메인에서 가능한 엄격한 수학적 검증을 받지 못한 채, 설계 결함이나 래더 로직 폭탄(Ladder Logic Bomb, LLB)과 같은 악성 코드 주입에 취약한 상태로 남게 된다.

방법론

본 논문은 ESBMC(Efficient SMT-based Context-Bounded Model Checker)의 새로운 프런트엔드로 구현된 오픈 소스 형식 검증기인 ESBMC-PLC를 제시한다. 방법론의 핵심은 표준 PLCopen XML(LD를 위한 개방형 인터체인지 형식)에서 ESBMC의 내부 GOTO-중간 표현(GOTO-IR)으로의 직접적인 번역 파이프라인이다.

핵심 아키텍처

입력 파싱: 이 도구는 주요 벤더(Siemens, Rockwell, CODESYS, OpenPLC)에서 내보낸 PLCopen XML 파일(텍스트 및 그래픽 tc6_0201 형식 모두 포함)을 수용한다. 수동 편집 없이 참조 ID를 통해 회로 토폴로지를 재구성한다.
GOTO-IR로의 번역:
- 스캔 사이클 모델링: PLC 실행 모델은 while(true) 루프로 인코딩된다.
- 상태 관리: 입력 변수는 매 반복마다 비결정론적으로 재샘플링된다(개방형 세계 센서 환경 모델링). 출력 코일 및 내부 마커는 정적 지속 변수로 모델링되어 스캔 사이클 간에 상태를 유지한다.
- 요소 매핑: LD 요소(XIC/XIO 접점, OTE/OTL/OTU 코일, TON/TOF/TP 타이머, CTU/CTD 카운터)는 GOTO-IR 연산으로 번역된다. 번략 규칙은 특히 래치 우선순위(OTL/OTU) 및 에지 트리거 카운터와 관련하여 Ebnenasir [9]가 정의한 공식 의미론(semantics)과 일치하도록 설계되었다.
- 데이터 타입: IEC 61131-3 타입은 가장 작은 C 대응 타입으로 매핑된다(예: BOOL은 bool로, TIME은 밀리초를 나타내는 uint32_t로).
속성 명세: 엔지니어가 템포럴 로직(temporal logic)에 대한 전문 지식 없이도 다섯 가지 유형의 안전 속성(mutual_exclusion, invariant, absence, response, reachability)을 지정할 수 있도록 하는 YAML 기반 언어를 제공한다.
검증 엔진: 백엔드는 Z3 SMT 솔버를 사용하는 ESBMC를 활용한다. 다음을 지원한다:
- 증분 BMC(Incremental BMC): 안전하지 않은 프로그램에서 빠르게 버그를 찾는 데 사용된다.
- k-유도(k-Induction): 수동 루프 언롤링 없이 모든 가능한 스캔 사이클에 대해 속성을 검증하여 무제한 안전 증명을 수행한다.

주요 기여

최초의 네이티브 LD 프런트엔드 오픈 소스: ESBMC-PLC는 표준 PLCopen XML 형식의 IEC 61131-3 LD 프로그램을 네이티브로 수용하는 최초의 오픈 소스 도구로, C나 ST로의 수동 번역 필요성을 제거한다.
LD를 위한 무제한 증명: LD 프로그램에 k-유도를 적용하여, 단순한 유계 모델 체킹(bounded model checking)에 의존하는 대신 무제한 안전 증명을 가능하게 한 최초의 도구이다.
실행 가능한 반례(Counterexamples): 도구는 원래의 LD 변수 이름을 참조하는 반례를 생성하여 자동화 엔지니어가 즉시 해석할 수 있도록 한다.
체계적인 격차 분석: 22개의 연구(2020–2026)에 대한 조사를 통해 네 가지 연구 격차를 식별하였으며, ESBMC-PLC는 오픈 소스 LD-to-formal 번역기의 부재와 IEC 61131-3을 위한 ESBMC 프런트엔드의 부재 문제를 직접 해결한다.
벤치마크 세트: 저자들은 6개의 산업 도메인과 3가지 출처(원본, 합성, 실제 벤더 프로그램)에 걸친 13개의 벤치마크를 도입하였다. 여기에는 CONTROLLINO 및 MathWorks의 수정되지 않은 프로그램이 포함된다.

실험 결과

평가는 6개의 산업 도메인(모터, 운송, 안전, 인프라, 식품 산업, 건물)에 걸친 13개의 벤치마크(안전 7개, 불안전 6개)를 대상으로 수행되었다.

분류 정확도: ESBMC-PLC는 13개의 벤치마크를 모두 정확하게 분류하였으며, 오탐(false positive)과 미탐(false negative)이 모두 0이었다. 여기에는 저자에 의해 사전 라벨링되지 않은 4개의 독립적인 벤더 프로그램(카테고리 C)이 포함되었다.
버그 탐지: 도구는 불안전한 변형 모델에서 8개의 뚜렷한 버그를 식별하였다. 여기에는 다음이 포함된다:
- 비상 정지 시 타이머 리셋 실패(CS2).
- 비상 차단 신호를 무시하는 리셋 로직(CS3).
- 신호등의 동시 위상 활성화에 대한 인터록 누락(CS4).
- 문 열림 신호가 모터 시작과 동일한 스캔 사이클에서 활성화되는 레이스 컨디션(CS8).
- 센서 결함 조건 하에서 펌프와 밸브의 동시 활성화(CS12).
성능: 61개의 속성 체크가 Apple Silicon (aarch64)에서 60ms 미만에 완료되었다.
무제한 증명: 7개의 안전한 프로그램 모두 k-유도를 사용하여 검증되었으며( $k=2$ 에서 수렴), 무조건적인 안전 보장을 제공하였다.
실제 환경 검증: 이 도구는 전처리 없이 CONTROLLINO 저장소 및 MathWorks Simulink PLC Coder 문서의 실제 프로그램을 성공적으로 파싱하고 검증하였다.

의의 및 주장

본 논문은 ESBMC-PLC가 산업용 PLC 래더 로직의 형식 검증이 자동화 엔지니어가 접근 가능한 실용적이고, 오픈 소스이며, 1초 미만이 소요되는 작업임을 입증한다고 주장한다.

독보적 위치: 최신 기술인 PLCverif(CBMC에 의존하며 ST/SCL 입력을 요구함)와 달리, ESBMC-PLC는 네이티브 LD 입력, k-유도 무제한 증명, 그리고 SMT 비트 벡터 의미론을 결합한 유일한 오픈 소스 도구이다.
실질적 영향: 전통적인 기능 테스트가 놓치는 버그(센서 결함 시나리오 및 스캔 사이클 순서에 의존하는 레이스 컨디션 등)를 탐지함으로써, 이 도구는 산업 제어 시스템의 중요한 안전 격차를 해소한다.
한계 및 범위: 저자들은 번역 규칙이 Ebnenasir의 의미론에 대해 경험적으로 검증되었으나, IEC 61131-3 표준과 완전히 동일함을 공식적으로 증명한 것은 아니라고 겸허히 언급하였다. 현재 구현은 핵심 서브셋(REAL/FLOAT, 문자열, 배열 및 멀티 POU 제외)을 다루며, 아직 인터럽트 태스크와 같은 벤더 특정 확장 기능을 지원하지 않는다.

논문은 결론적으로 ESBMC-PLC가 PLC 검증의 중요한 연구 격차를 메우고 있으며, ESBMC-PLC의 LD 프런트엔드와 PLCverif의 ST 파이프라인을 통합하는 통합 플랫폼이 산업급 검증을 위한 논리적인 미래 방향임을 시사한다.