비동기 스트림 방정식(Asynchronous Stream Equations)을 위한 페이싱 타입(Pacing Types)

스트림 기반 모니터링(Stream-based monitoring)은 모니터가 센서 및 기타 소스로부터 입력 데이터의 스트림을 집계하여 시스템 상태에 대한 실시간 통계와 평가를 제공하는 런타임 검증(runtime verification) 접근 방식입니다. 신뢰할 수 있는 스트림 기반 모니터를 설계할 때 직면하는 핵심 과제 중 하나는 데이터 스트림의 비동기적(asynchronous) 특성을 다루는 것입니다. 구체적인 애플리케이션에서 모니터링되는 서로 다른 센서들은 서로 다른 속도로 값을 생성하며, 서로 다른 값의 스트림이 비동기적으로 도착할 때 이에 올바르게 반응하는 것은 모니터의 책임입니다. 이 과정을 완화하기 위해 RTLola와 같은 현대적인 스트림 기반 모니터링 프레임워크는 사용자가 페이싱 어노테이션(pacing annotations) 시스템을 통해 데이터 동기화 정책을 세밀하게 지정할 수 있도록 지원합니다. 이러한 기능은 모니터 설계를 단순화하지만, 사용자가 일관성 없는 정책을 작성하게 만들 수도 있습니다. 즉, 어노테이션을 통해 두 스트림 간의 동기화를 명시적으로 요청했으나 이를 항상 달성할 수 없는 경우가 발생할 수 있습니다. 이 문제를 완화하기 위해, 본 논문은 비동기 스트림을 위한 모니터가 타이밍 불일치(timing inconsistencies)가 없음을 보장하기 위해 RTLola에 구현된 새로운 타입 시스템인 페이싱 타입(pacing types)을 제시합니다. 우리는 RTLola의 핵심 파편(core fragment)에 대한 페이싱 어노테이션의 형식적 의미론(formal semantics)을 제공하고, 페이싱 타입 시스템의 건전성 증명(soundness proof)을 제시합니다. 추가적인 보증 수준을 위해, 우리는 Rocq 증명 보조기(proof assistant)를 사용하여 건전성 증명을 기계적으로 검증(machine-checked)하였습니다.