안전 사양을 위한 시나리오 기반 구성 통계 모델 검사

자율 주행과 같은 안전 필수 영역에서는 시스템이 종종 기본(primitive) 시나리오로부터 구축된 복합 시나리오(composite scenarios)로 표현되는 방대한 수의 환경 조건에 걸쳐 평가되어야 합니다. 기존의 통계 모델 검사(Statistical Model Checking, SMC) 접근 방식은 각 복합 시나리오를 독립적으로 분석하여 많은 비용이 드는 시뮬레이션을 요구하며, 이 과정에서 시나리오들이 공통 구조를 공유할 때 상당한 중복 계산을 초래합니다. 본 연구는 안전 및 공동 안전 사양(co-safety specifications)을 위한 시나리오 기반 구성 SMC 프레임워크를 소개하여 복합 시나리오의 효율적인 분석을 가능하게 합니다. 저희 접근 방식은 시나리오를 기본 요소로, 사양을 하위 사양으로 분해하고, 각 기본 요소를 독립적으로 검증하며, 중요도 샘플링(importance sampling)과 커널 밀도 추정(kernel density estimation)을 사용하여 결과적인 통계적 추정치를 구성합니다. 저희의 경험적 평가는 제안된 프레임워크가 병렬화 및 트레이스 재사용을 통해 시뮬레이션 비용을 줄이면서, 이전에 보지 못한 복합 시나리오에 대한 검증 질의에 정확하게 답변할 수 있음을 보여줍니다.