기술 요약: Lola에서의 런타임 검증 및 모델 기반 진단을 위한 통합 프레임워크

문제 정의

안전 필수 시스템(Safety-critical systems)은 단순히 실패를 탐지하는 것을 넘어, 효과적인 완화를 가능하게 하기 위해 그 근본 원인을 국소화(localization)할 수 있어야 한다. **런타임 검증(Runtime Verification, RV)**은 실행 중 명시된 동작으로부터의 이탈을 탐지하는 데 효과적이며, **모델 기반 진단(Model-Based Diagnosis, MBD)**은 결함이 있는 구성 요소를 식별하기 위한 원칙적인 프레임워크이다. 그러나 이 두 기술은 역사적으로 서로 분리되어 운영되어 왔다. 전통적인 RV 모니터는 위반을 탐지하기 위해 잠재적으로 무한한 상태 시퀀스에 걸쳐 시스템 동작을 분석하는 반면, MBD는 일반적으로 결함이 탐지된 후의 특정 시점에서 작동한다. 더욱이, 기존의 통합 방식들은 탐지된 실패 동작을 MBD 관점의 비정상 구성 요소로 직접 매핑하지 못하거나, 불확inc한 입력 및 시간적 결함 역학을 통합된 스트림 기반 추론 프레임워크 내에서 처리하는 데 한계가 있다.

방법론

본 논문은 스트림 기반 명세 언어인 Lola 내에서 스트림 기반 RV와 MBD를 통합하는 통합 프레임워크를 제안한다. 핵심 방법론은 진단된 시스템 $S = (sd, comps)$를 Lola 시스템 $(\phi, comps)$로 인코딩하는 것이며, 이를 통해 진단 정보와 검증 정보를 특수화된 스트림으로 표현하여 불확실성 하에서도 지속적인 관찰과 기호적 추론을 가능하게 한다.

1. Lola에서의 통합 인코딩

저자들은 진단된 시스템 $S = (sd, comps)$를 다음과 같이 Lola 시스템 $(\phi, comps)$로 매핑한다:

• **시스템 기술 ($sd$):** 정의에 의해 참인 **가정 스트림($\alpha$)**으로 인코딩된다. 이 스트림은 행동 지식(예:$ \neg ab(c) \to beh_c $) 및 시스템에 대한 일반적인 지식을 포함한다.
• **구성 요소 ($comps$):** 각 구성 요소$c$는 구성 요소가 비정상($ab(c)$)임을 나타내는 true를 갖는 내부 불리언 스트림으로 표현된다.
• 관측(Observations): 관측 가능한 시스템 변수(입력/출력)는 입력 스트림으로 모델링되며, 이는 결정론적이거나 불확실한(비결정론적 구간 또는 집합) 형태를 가질 수 있다.
• 관측 불가능한 변수: 직접 측정되지 않는 내부 시스템 값은 내부 스트림으로 모델링된다.
• 진단 문제 인스턴스 (DPI): 튜플 $(\phi, comps, \Psi)$로 정의되며, 여기서 $\Psi$는 현재 시점까지의 입력 제약 조건의 이력을 나타낸다.

2. 기호적 추론 및 진단 계산

프레임워크는 현재 시점 $t$까지의 관측값과 일치하는 모든 가능한 시스템 동작을 나타내는 제약 집합 $[\phi]_{\Psi}^{\leq t}$를 유지하는 **기호적 모니터(symbolic monitor)**를 활용한다.

• 제약 해결(Constraint Solving): 일관성을 확인하고 함축(entailment)을 도출하기 위해 SMT 솔버(예: Z3)가 사용된다.
• 진단 도출: 진단은 관측값과 시스템 기술을 일치하게 만드는 상태(정상/비정상)에 대한 가정이다. 프레임워크는 최소 충돌(모두 정상일 수 없는 구성 요소 세트)을 식별하고 이들의 **최소 히팅 세트(minimal hitting sets)**를 계산함으로써 최소 진단을 산출한다.
• 가지치기(Pruning): 상수 시간 및 상수 공간 모니터링을 보장하기 위해, 제약 집합의 크기를 제한하도록 제약 조건을 재작성하여 필요한 과거 정보만을 유지하는 가지치기 전략을 사용한다.

3. 진단 시나리오

프레임워크는 구성 요소 결함의 시간적 특성에 따라 세 가지 별개의 진단 모드를 지원한다:

• 다중 인스턴트 진단 (Multi-Instant Diagnosis): 구성 요소 상태가 과거 $k$개의 인스턴트($t-k$부터 $t$까지) 동안 정적이라고 가정한다. $k$-인스턴트 진단은 이 윈도우 내의 모든 관측값을 설명한다. 논문에서는 비시간적(atemporal) 명세의 경우 $k$-인스스턴트 진단이 단일 인스턴트 진단의 집합과 동일함을 증명하지만, 시간적(temporal) 명세(오프셋이 0이 아닌 경우)의 경우에는 더 집중된 결과를 제공한다.
• 시간적 진단 (Temporal Diagnosis): 구성 요소 상태가 시간에 따라 변하는 것을 허용한다. $k$-시간적 진단은 구성 요소 $c$가 특정 시점 $t'$에 비정상임을 나타내는 쌍 $(c, t')$의 집합이다. 이는 과열과 같은 일시적 결함이나 전파로 인해 나중에 나타나는 결함을 식별하는 데 중요하다.
• 확장 설정 (Extended Settings): 배경 지식(구성 요소를 정상으로 강제함), 강력한 결함 모델(특정한 결함 동작을 명시함), 그리고 추상적 모델링을 자연스럽게 통합한다.

주요 기여

1. 통합 인코딩: 관측된 동작에 대한 모든 유효한 진단을 암시적으로 표현하기 위해, 시스템 기술과 진단 가정을 Lola의 특수화된 스트림으로 표현하는 방법.
2. 다중 인스턴트 진단 이론: 표준적인 다중 관측 진단을 특수 사례로 포괄하는, 슬라이딩 윈도우 관측에 대한 불변적 결함 진단의 일반화된 이론.
3. 시간적 진단: 어떤 구성 요소가 결함인지뿐만 아니라 언제 결함이 발생하는지를 식별할 수 있도록 시간 가변적 비정상성을 지원함.
4. 유연한 진단 시나리오: 단일 스트림 기반 프레임워크 내에서 배경 지식, 추상적 모델링 및 다양한 결함 유형(지속적 vs 일시적)을 우아하게 처리할 수 있는 능력.
5. 구현 및 평가: ISCAS85 및 ISCAS89 벤치마크를 통해 검증된, HS-Tree 알고리즘, QuickXplain 및 Z3가 통합된 프로토타입 구현.

결과

저자들은 두 개의 불리언 회로에 대해 프레임워크를 평가하였다:

• c17 (ISCAS85): 6개의 구성 요소를 가진 순수 조합 회로.
• s27 (ISCAS89): 14개의 구성 요소를 가진 순차 회로.

주요 결과:

• 실행 가능성: 프레임워크는 두 회로 모두에서 주입된 실제 결함(stuck-at-false)을 성공적으로 식별하였다.
• 시간적 정확도: 순차 회로(s27)의 경우, 관측 윈도우($k$)가 결함의 기점과 전파 시간을 포함할 만큼 충분히 클 때만 프로임워크가 결함을 정확하게 국소화하였다.
• 성능:
  • 런타임은 더 큰 $k$ 값에 따라 증가하였다. c17의 경우, $k$-인스턴트 진단은 인스턴트당 최대 246 ms ($k=0$)에서 775 ms ($k=31$)가 소요되었다.
  • 시간적 진단은 $(c, t')$를 별개의 구성 요소로 취급함에 따른 조합 폭발로 인해 훨씬 더 많은 비용이 발생하였다. c17의 경우, 시간적 진단은 $k=5$일 때 인스턴트당 최대 8.7초, $k=12$일 때 136초가 소요되었다.
  • 이러한 계산 비용에도 불구하고, 저자들은 $k$가 상수일 경우 런타임이 전체 트레이스 길이에 독립적임을 언급하며, 이는 가지치기 전략의 타당성을 확인해 준다고 밝혔다.

의의 및 주장

본 논문은 런타임 검증과 모델 기반 진단을 결 một 조밀하고 근거 있는 통합을 제공한다고 주장한다. 이 연구의 의의는 단일 스트림 기반 프레임워크 내에서 자동화된 결함 탐지(RV)와 체계적인 결함 국소화(MBD) 사이의 간극을 메우는 데 있다.

저자들은 이 접근 방식이 다음을 수행함을 강조한다:

• 불확실한 입력 및 환경 가정을 지원하여, 전문가 지식에 기반한 정교한 추론을 가능하게 한다.
• 각 시점마다 판결(verdict)을 생성하기 위해 기호적 추론을 활용함으로써 온라인 진단을 가능하게 한다.
• RV의 강점(효율적이고 지속적인 모니터링)과 MBD의 강점(원칙적인 근본 원인 분석)이 결합된 시너지 효과를 제공한다.
• 제약 조건에 의해 정의된 모든 가능한 세계와 일치하는 값을 기호적 모니터가 보장하는 건전한(sound) 프레임워크를 제공한다.

본 연구는 Lola를 복잡한 진단 작업에 사용하는 것이 가능하다는 것을 보여주는 개념 증명(proof-of-concept)으로서, 안전 필수 시스템을 위한 미래의 실질적 응용을 위한 이론적 토대를 제공한다.