Synchronous Observers Revisited for Runtime Verification of Lustre Using STL

기술 요약: Lustre를 이용한 런타임 검증을 위한 동기식 옵저버 재고찰

문제 정의
신호 템포럴 로직(Signal Temporal Logic, STL)은 사이버 물리 시스템(CPS), 특히 런타임 검증을 위한 시간적 안전성 속성을 명시하는 표준 형식론이다. 그러나 기존의 STL 도구들은 대개 실제 배포된 실행 가능한 코드보다는 사전 기록되거나 시뮬레이션된 신호, 또는 추상적인 오토마타 모델 위에서 동작한다. 결과적으로, 모니터링되는 시스템과 락스텝(lock-step)으로 실행되는 중첩된 STL 속성에 대한 실행 가능한 런타임 등가 세맨틱(semantics)이 부족한 실정이다. 더욱이, 동기식 언어인 Lustre는 정적 검증을 위해 "동기식 옵저버(synchronous observers)"를 사용하지만, 이러한 옵저버를 런타임 검증에 활용하는 잠재력은 충분히 탐구되지 않았다. 구체적인 과제는 온라인 모니터링의 "3치(three-valued)" 특성을 처리하는 것이다. 유계된(bounded) 템포럴 연산자는 미래를 내다보기 때문에, 모니터는 매 틱(tick)마다 즉각적으로 결론을 내릴 수 없으며, 확정적인 판결에 도달하기까지 지연이 발생할 수 있다.

방법론
저자들은 동기식 STL(SSTL)의 동기식 파편(synchronous fragment)을 Lustre 내의 동기식 옵저버로 직접 컴파일하는 기법을 제안한다. 핵심 방법론은 중첩된 공식들을 고정된 이산 시간 틱(discrete time ticks)의 윈도우를 모니터링하는 비중첩된 유한한 의무(obligations)들의 집합으로 "언롤링(unrolling)"하는 것이다.

1. 3치 스트리밍 세맨틱: 본 접근 방식은 클레네 3치 세맨틱(def_true, def_false, unknown)을 채택한다. 각 틱에서 옵저버는 지금까지 관찰된 접두사(prefix)를 기반으로 판결을 방출한다. unknown은 공식의 호라이즌(horizon)이 아직 경과하지 않았음을 나타낸다. 이는 확정적 참과 확정적 거짓을 나타내는 두 개의 불리언 신호 쌍 (pos, neg)를 사용하여 구현된다.
2. 기본 구조 (until_leaf): 저자들은 유계된 "until" 연산자($U_{[a,b]}$)를 구현하는 재사용 가능한 단일 Lustle 노드인 until_leaf를 합성한다. 이 프리미티브(primitive)는 특정 윈도우 동안 전제 조건("alive" 신호)과 후속 조건("found" 신호)을 추적한다. 이는 증거(witness)를 발견하면 def_true를 방출하고, 전제 조건 실패 또는 윈도우 만료 시 def_false를 방출한다.
3. 재귀적 합성: 중첩된 공식들은 바텀업(bottom-up) 방식으로 합성된다. 시스템은 외부 연산자에 필요한 모든 시작 오프셋에 대해 until_leaf 프리미티브의 복사본을 인스턴스화한다. 이 복사본들은 클레네 논리 규칙(conjunction, disjunction, negation)을 사용하여 서로 연결된다.
   • 유계 연산자($\square_{[a,b]}$, $\diamond_{[a,b]}$)의 경우, 합성은 각 구간 내의 각 시작 오프셋에 해당하는 리프(leaf)들로 공식을 언롤링한다.
   • 자유 주행 시스템(free-running systems)에서 흔히 사용되는 무계(unbounded) Globally 연산자($\square$)의 경우, 저자들은 시프트 레지스터(shift-register) 구조를 도입한다. 무한한 옵저버를 인스턴스화하는 대신, 내부 호라이즌 $H$와 $H+1$ 크기의 레지스터를 사용하여 상태를 재순환(recycle)함으로써, 모니터가 내부 공식의 "alive" 복사본들을 지속적으로 추적할 수 있게 한다.
4. 시각화: 편집 가능한 트레이스 상에서 중첩된 옵저버의 3치 판결을 렌더링하여 복잡하고 중첩된 템포럴 동작에 대한 디버깅과 직관을 돕는 인터랙티브 브라우저 기반 도구가 제공된다.

주요 기여

1. 실행 가능한 온라인 모니터링: 본 기법은 시스템과 동일한 동기식 언어(Lustre)로 컴파일되어, 시뮬레이션된 데이터가 아닌 실제 실행 가능한 코드와 락스텝으로 실행되는 옵저버를 합성한다.
2. 모듈형 컴파일을 통한 임의의 중첩 지원: 비중첩 연산자로 제한되었던 기존 연구(Bellanger et al.)와 달리, 본 방법은 임의로 중첩된 유계 SSTL 속성을 지원한다.
3. 무계 외부 연산자: 본 접근 방식은 내부 구조를 유계로 유지하면서도, 자유 주행 시스템 모니터링에 적합한 전역 무계 외부 연산자($\square$)를 허용한다.
4. 이중 용도: 생성된 옵저버는 런타임 모니터로 기능하는 동시에, 별도의 모델 없이 Kind2 모델 체커를 위한 정적 검증 의무(static verification obligations)로서의 부수적 기능도 수행한다.
5. 런타임을 위한 3치 세맨틱: 구현된 인과적 클레네 판결(causal Kleene verdicts)을 통해, 모니터가 전체 공식 호라이즌이 도달하기 전이라도 트레이스가 허용하는 한 조기에 확정적인 답변을 내릴 수 있도록 한다.

결과 및 평가
저자들은 스프링-질량 시스템(spring-mass system)과 긴급 제동 상황의 차량 추종 적응형 크루즈 컨트롤(ACC) 시나리오라는 두 가지 사례 연구를 통해 기술을 평가하였다.

• 정확성: 합성된 모든 옵저버는 Kind2 모델 체커를 통해 검증되었다. 런타임 판결과 정적 판결은 상호 배제 불변량($pos \land neg = \text{false}$)을 포함한 모든 속성에 대해 일치하였다.
• 성능: 옵서버들은 C로 컴파일되어 lv6 인터프리터를 통해 실행되었다. 틱당 실행 비용은 복잡도에 따라 약 6.7 ns에서 206.5 ns 사이로 측정되었으며, 이는 일반적인 밀리초 단위의 제어 주기보다 훨씬 낮아 온라인 배포 가능성을 확인시켜 주었다.
• 조기 종료: 3치 세맨틱은 효과적임이 입증되었다. 사례 연구에서 유계된 속성들은 이론적 호라이즌보다 엄격하게 앞서 확정적 판결에 도달했다. 예를 들어, 깊게 중첩된 속성($P3$)은 15 틱 일찍 판결이 완료되었다.
• 무계 동작: 무계 $\square$ 연산자는 반례(violation)가 발생했을 때 올바르게 def_false로 래치(latch)되고 그 외에는 unknown으로 유지되는 반례 전용 메커니즘으로서 기능하였다.

의의 및 주장
본 논문은 공식 명세와 실행 가능한 런타임 모니터링 사이의 간극을 메운다고 주장한다. 시스템의 언어로 직접 옵저버를 합성함으로써, 저자들은 배포된 코드와 추상 모델 간에 흔히 발생하는 "모델링 격차"를 제거한다. 본 연구는 복잡하고 중첩된 템포럴 속성이 낮은 지연 시간과 높은 신뢰도로 온라인에서 모니터링될 수 있음을 보여준다. 저자들은 본 작업을 Bellanger et al. [5]의 확장판으로 위치시키며, 특히 중첩 깊도에 대한 제한과 정적 검증 중심의 방향성을 해결하였다. 이 기법은 명시적인 3치 세맨틱에 대해 건전하고 완전한(sound and complete) 체계적인 합성 기술로 제시되며, 런타임 실행과 정적 모델 체킹을 통해 검증되었다.

한계점
저자들은 세 가지 주요 한계를 인정한다:

1. 상태 폭발(State Explosion): 리프(leaf)의 수는 윈도우 너비의 곱이므로, 큰 구간(예: $\diamond_{[0,100]}$)에 대해 옵저버의 크기가 기하급급수적으로 증가할 수 있다.
2. 폐쇄형 시스템 가정: 사례 연구들은 Lustre 내에서 플랜트를 폐쇄형 시스템으로 모델링하였다. 외부 센서 입력을 가진 실제 개방형 시스템을 모니터링하는 것은 향후 과제로 남아 있다.
3. 이산 도메인: 현재의 접근 방식은 엄격하게 샘플링되고 이산화된 도메인 내에서 작동하며, 아직 연속적인 STL 강건성(robustness) 세맨틱을 지원하지 않는다.