OpenPLC, Arduino OPTA, CONTROLLINO, 그리고 Industrial Shields M-Duino는 실제 자동화 및 산업 제어 시스템(ICS) 보안 연구에 사용되는 저가형 마이크로컨트롤러에 IEC 61131-3을 구현합니다. ESBMC-PLC를 포함한 기존의 IEC 61131-3 오픈 소스 검증기는 이상적인 무한 정수(unbounded integers)를 가진 추상 스캔 사이클 모델 위에서 안전성을 증명합니다. 그러나 이 보드 아티팩트는 16비트 워드(8비트 AVR Arduino)를 사용하는 리소스 제약형 마이크로컨트롤러 유닛(MCU)에서 실행되며, 센서는 유한 해상도의 아날로그-디지털 변환기(ADC)를 통해 읽힙니다. 우리는 이러한 배포 격차(deployment gap)가 순진한 너비 인식 검증(width-aware verification)을 불안정하게 만든다는 것을 보여줍니다: 123개의 실제 프로그램에 걸쳐, 하드웨어 입력 모델 없이 16비트 오버플로우를 확인하는 것은 44%의 거짓 경보(54/123)를 발생시키고 실제 결함을 발견하지 못합니다. 그 이유는 그것이 ADC가 생성할 수 없는 센서 값을 탐색하기 때문입니다. 이 격차는 계산이 물리적 프로세스를 만나는 지점, 즉 유한 너비 산술로 스케일링된 경계형 센서 판독값이 작동 명령으로 변환되는 곳에 존재하며, 오버플로우가 고수준 알람과 같은 안전 조치를 조용히 억제할 수 있습니다. 무한 입력 모델은 어떤 환경도 트리거할 수 없는 알람을 꾸며냅니다. 우리는 오픈 하드웨어에서 IEC 61131-3에 대한 하드웨어 충실 검증(hardware-faithful verification)을 제시합니다: 선언적 하드웨어 추상화 계층(HAL) 디스크립터(너비, ADC/PWM 해상도, I/O 바인딩)와 목표 너비에서 산술을 해석하고 입력을 하드웨어 구현 가능한 범위로 제약하는 건전한 낮추기(sound lowering)입니다. 우리는 이를 ArduinoTool로 인스턴스화하여 공식 코어로부터 HAL 매개변수를 파생시키고 ESBMC 래더 다이어그램(LD) 프론트엔드에서 입력 범위 모델을 실현합니다. 123개 프로그램 코퍼스에서, HAL 주석기는 모든 54개의 거짓 경보를 제거하는 동시에 견고성 증명(robustness proofs)을 유지하며, 제어된 코퍼스는 그것이 구현 가능한 증거(realizable witnesses)와 함께 감지하는 희귀한 너비 의존적 결함을 입증합니다.