UPPAAL: Real-Time Timed Automata 모델 검증 도구

1. UPPAAL 개요

UPPAAL은 덴마크 Aalborg University와 스웨덴 Uppsala University가 개발한 실시간 시스템용 Timed Automata 모델링 및 모델 체커입니다. 임베디드 제어기, 통신 프로토콜, 사이버-물리 시스템(CPS) 등에서 시간 제약을 포함한 동작의 안전성·응답성·데드록 여부를 분석하는 데 널리 사용됩니다.

본 연구에서는 CPS의 소프트웨어 요구사항과 운영 환경을 UPPAAL에서 Timed Automata로 모델링하고, 여기서 검증된 결과를 기반으로 TADA → Go 코드 → 런타임 모니터로 연결하는 TA–TADA–to–Go 파이프라인의 출발점으로 사용합니다.

2. UPPAAL의 주요 특징

  • 그래픽 기반 모델링: 위치(location), 전이(transition), clock, invariant를 GUI에서 직관적으로 편집할 수 있습니다.
  • Timed Automata 네트워크 지원: 여러 automaton 인스턴스를 병렬로 구성하고, 채널(channel) 동기화를 통해 상호작용을 모델링합니다.
  • 시뮬레이션 & 디버깅: 모델을 step-by-step으로 실행해 보고, clock 값과 변수 값을 추적하면서 설계 오류를 조기에 발견할 수 있습니다.
  • 모델 체킹(Verification): TCTL의 부분집합으로 구성된 UPPAAL 쿼리 언어를 통해 도달 가능성, 안전성, 응답성, 데드록 부재 등을 자동 검증합니다.
  • CPS 사례에 적합한 확장: integer / bool 변수, urgent / committed location, broadcast channel 등 실제 시스템에 가까운 모델링을 위한 다양한 확장을 제공합니다.

3. 모델링: Timed Automata 네트워크 문법

UPPAAL에서 하나의 시스템은 Timed Automata 네트워크로 표현됩니다. 각 automaton은 다음 요소로 이루어집니다.

  • Locations: 시스템의 추상 상태를 나타내는 노드
  • Edges (Transitions): guard, synchronisation, update를 포함하는 전이
  • Clocks: 실시간 제약을 표현하는 연속 변수
  • Invariants: 각 location에서 허용되는 clock 범위
  • Data variables: int, bool 등 이산 상태 변수

전이는 다음과 같은 형식으로 구성됩니다.

// edge: source --[guard, sync, update]--> target
source -- [ x <= 5,   press?,   y := 0 ] --> target
  • guard: 전이가 활성화되기 위한 clock/변수 조건 (예: x > 5)
  • sync: press?, press!와 같은 채널 동기화
  • update: clock reset 및 변수 갱신 (예: y := 0)

4. 검증 쿼리 언어 (UPPAAL Query Language)

UPPAAL은 TCTL의 부분집합 기반 쿼리 언어를 사용합니다. 대표적인 연산자는 다음과 같습니다.

  • A[] ϕ : 모든 실행 경로에서 항상 ϕ가 성립 (safety)
  • E<> ϕ : 어떤 실행 경로에서는 언젠가 ϕ에 도달 (reachability)
  • A<> ϕ : 모든 실행 경로에서 언젠가 ϕ에 도달 (liveness)
  • E[] ϕ : 어떤 실행 경로에서는 항상 ϕ가 유지

본 연구에서는 이러한 쿼리를 이용해 타이밍 제약, 데드록 부재, 응답 시간 등 CPS 요구사항을 TA 모델 수준에서 먼저 검증합니다.

5. 의미론과 분석 기능

UPPAAL의 의미론은 Timed Automata 네트워크에 대한 상태 공간으로 정의됩니다. 하나의 상태는 각 automaton의 위치와 clock/변수 값을 포함하는 튜플입니다.

  • 상태 = (loc1, ..., locn, v) – 각 loci는 i번째 automaton의 location, – v는 모든 clock과 데이터 변수의 값.
  • 시간 진행과 이산 전이가 결합된 hybrid transition system을 구성.
  • 상태 공간을 symbolic하게 표현하기 위해 zone, DBM을 사용하여, 실수 clock에 대해 무한한 시간 영역을 효율적으로 탐색.

이러한 의미론과 symbolic 기술 덕분에, UPPAAL은 복잡한 CPS 모델에 대해서도 시간 관련 속성을 자동으로 검증할 수 있습니다.

6. TA–TADA–to–Go 프레임워크에서의 UPPAAL 역할

TA–TADA–to–Go 프레임워크에서 UPPAAL은 다음과 같은 역할을 수행합니다.

  • CPS의 소프트웨어 요구사항과 운영 환경을 Timed Automata로 모델링하는 프런트엔드 도구 역할
  • Timed-CTL 기반 쿼리를 통해 안전성, 데드록 부재, 응답 시간 등을 사전에 검증하고, 모델 수준에서 오류를 제거
  • 검증이 끝난 TA 모델을 TADA 변환기의 입력으로 제공하여, 이후 TADA → Go 코드 → 런타임 모니터로 이어지는 자동화된 코딩·모니터링 파이프라인의 신뢰성을 보장

7. 결론: CPS 신뢰성 검증을 위한 표준 도구

UPPAAL은 실시간 시스템의 정형 모델링과 자동 검증을 위한 사실상의 표준 도구로, TA–TADA–to–Go 프레임워크에서도 타임드 오토마타 기반 요구사항 검증의 기반을 제공하는 핵심 구성 요소입니다. UPPAAL에서 검증된 모델은 이후 TADA로 정규화되고, Go 코드와 런타임 모니터로 자동 변환됨으로써 형식 검증에서 실제 실행 환경까지 일관된 신뢰성 보증을 가능하게 합니다.