ESBMC-Arduino: 격차 해소로 공식 검증의 실효성 확보

ESBMC-Arduino: Closing the Deployment Gap for Formal Verification

OpenPLC, Arduino OPTA, CONTROLLINO, Industrial Shields M-Duino 등 저비용 MCU 기반 산업용 제어 시스템에서 IEC 61131-3 프로그래밍이 가능해졌지만, 기존 ESBMC-PLC와 같은 검증 도구는 추상적 스캔 사이클 모델과 이상적인 무한 정수 산술을 가정해 실제 하드웨어와의 괴리가 있었습니다. 연구진은 123개 실제 프로그램 분석을 통해 16비트 오버플로우 검사 시 하드웨어 입력 모델이 없으면 44%의 오탐(false alarm)이 발생하고 실제 결함은 발견하지 못함을 보였습니다. 이러한 배포 격차를 해소하기 위해 하드웨어 추상화 계층(HAL) 설명자와 하드웨어 실현 가능한 입력 범위를 적용하는 사운드 러워링을 제안하고, Arduino용 ArduinoTool로 구현했습니다. 그 결과 54개 오탐을 모두 제거하면서 강건성 증명을 보존했고, 드물게 발생하는 너비 의존 결함을 실제 가능한 시나리오로 탐지할 수 있음을 입증했습니다.