Simulink 모델 체커의 비트 정밀 일치성 테스트 (Bit-Precise Conformance Testing)

MATLAB/Simulink는 사이버 물리 시스템 (cyber-physical systems) 개발을 위한 실용적인 모델링 언어와 시뮬레이션 엔진을 제공합니다. 개발된 모델의 품질을 보장하기 위해 Simulink Design Verifier (SLDV) 및 제3자 SMT 기반 모델 체커 (SmtMC)와 같은 형식 검증 (formal verification) 도구들을 사용할 수 있습니다. 그러나 모델의 모든 요소를 포괄하는 Simulink의 의미론 (semantics)과 수치적 동작 (numerical behavior)의 세부 사항이 부재하기 때문에, 모델 체커 자체의 신뢰성이 의심되는 경우가 많으며, 시뮬레이터와 다르게 모델을 분석할 가능성이 있습니다. 본 연구는 다음 항목들을 다룸으로써 Simulink 모델 체커의 품질을 검증하는 것을 목표로 합니다. 1) Simulink 기본 블록 타입의 형식화 (Formalization). 이는 블록 타입 기능 세트와 블록의 비트 정밀 (bit-precise) 동작을 정의하는 것을 포함합니다. 2) 각 블록 타입에 대해 도구 간의 비트 정밀 일치성 (bit-precise conformance) 관계를 테스트하는 방법. 우리 테스트 스위트의 통과율은 (i) 모델 체킹 결과와 Simulink 시뮬레이션 결과 간의 일치성, 그리고 (ii) SmtMC 결과와 SLDV 결과 간의 일치성을 측정합니다. 3) 10가지 블록 타입에 대해 테스트를 수행하는 실험. 우리는 SmtMC가 모든 테스트 케이스를 효율적으로 통과한 반면, SLDV는 일치성 (i)에 대해 94-96%, (ii)에 대해 80-90%의 통과율만을 달성했음을 확인했습니다. 우리는 오류, 코너 케이스 (corner cases), 타임아웃 (timeouts) 등 테스트 실패의 원인을 분석했습니다.