확률적 사양의 분해를 형식적으로 검증하기

초록 구성 검증 원칙에 따르면, 하위 구성요소가 자신의 사양을 만족하는지 검증하는 것은 전체 시스템이 최상위 사양을 만족하는 것을 보장합니다. 핵심 단계는 하위 사양이 최상위 사양의 올바른 분해를 구성하는지 확인하는 것입니다. 비확률적 맥락에서는 이러한 분해를 정리 증명 기법을 사용하여 분석할 수 있습니다. 산업 응용, 특히 안전-critical 시스템에서는 사양이 종종 확률적 특성을 가지며, 예를 들어 주어진 시간 이전에 시스템 오류가 발생할 확률에 대한 경계를 제공합니다. 이러한 사양의 분해는 전통적인 정리 증명 이상의 기술을 필요로 합니다. 이 논문의 첫 번째 기여는 시스템의 확률적 및 시간적 행동과 그러한 행동에 대한 사양을 표현하고 추론할 수 있는 이론적 프레임워크입니다. 이 프레임워크는 시스템의 연속 시간 진화를 설명하는 추적(trace)을 기반으로 하며, 사양은 확률적 수용 조건과 결합된 시간 오토마타를 사용하여 공식화됩니다. 두 번째 기여는 선형 부등식 시스템에 대한 해 공간의 공허성 확인 문제로 전환하여 이러한 사양의 분해를 검증하기 위한 새로운 접근 방식입니다.