JIN HYUN KIM

TADA: Timed Automata with Disjoint Actions

1. TADA의 등장 배경

기존 Timed Automata(TA)는 시간 진행(time progression)이 암묵적(implicit)이고, 위치(location)에 붙은 invariant와 guard가 뒤섞여 있어서 실제 코드로 변환할 때 시간 의미가 모호해지는 문제가 있다.

• action transition이 가능한데 시간도 동시에 흐르는 상황
• invariant (예: x ≤ n)를 어겼는지 런타임에서 감지하기 어려움
• 시간 조건(x == n 등)을 코드로 정확히 매핑하기 어려움

이를 해결하기 위해 논문에서는 TADA라는 새로운 중간 표현(Intermediate Formalism)을 도입한다. TADA의 목적은 다음 두 가지이다.

1. TA의 시간 의미를 완전히 드러내고(explicit) 구조화한다.
2. 코드 생성(특히 Go로의 자동 변환)이 가능한 형태로 정규화한다.

---

2. TADA의 핵심 특징

2-1. 위치(Location)를 Sub-location 단위로 분해

각 TA의 location을 시간 조건에 따라 여러 개의 sub-location으로 쪼갠다. 예를 들어 invariant가 x ≤ 60이고 guard가 x ≥ 5인 경우:

원래 location	TADA sub-location
Low	Low_0: 0 ≤ x < 5 Low_1: 5 ≤ x < 60 Low_2: x = 60 Low_3: x > 60 (violation)

이와 같이 분해하면 시간 흐름이 단계별로 명확하게 드러난다.

2-2. 시간 전이(Time transitions)와 동작 전이(Action transitions)의 완전 분리

기존 TA에서는 시간 전이와 동작 전이가 한 위치에서 얽혀 있어 모호하다. TADA에서는 다음과 같이 분리한다.

• Time transition: 오직 clock 조건 ec에 의해 발생
• Action transition: channel 동작 a(!/?), reset 집합 r에 의해 발생

시간과 동작의 책임이 분리되므로 구현이 단순해지고 의미가 명확해진다.

2-3. 시간 경계 조건의 명시화

TADA는 x == n, x > n, x ≤ n 등 TA 조건을 명시적인 sub-location 간 전이로 변환한다. 예를 들어 x == n은 "x가 정확히 n이 되는 그 순간"을 나타내는 별도의 sub-location으로 모델링된다.

2-4. Invariant 위반을 명시적 error state로 표현

TA에서는 invariant 위반이 "허용되지 않는 상태"로만 표현되지만, TADA에서는 violation sub-location을 명시적으로 생성한다. 실행 중 이곳에 도달하면 시간 제약 위반으로 인식하고, Go 모니터가 이를 감지하여 알람을 발생시키도록 설계한다.

2-5. Trace equivalence 유지

TADA로 변환하더라도 원래 TA와 동일한 observable trace를 보장한다. 따라서 형식적 검증 결과가 코드 생성 후에도 의미를 잃지 않는다.

---

3. TADA의 문법 (Syntax)

논문 정의(Definition 2)에 따르면 TADA는 다음과 같은 튜플로 정의된다.

TADA = ⟨L, l₀, X, A, E⟩

• L: location들의 집합 (각 location은 여러 sub-location을 가진다)
• l₀: 초기 location
• X: clocks
• A: actions
• E: 전이 집합
  • E_A: action transitions
  • E_T: time transitions

3-1. Action Transition

sl ─a,r→ l'

• sl: sub-location
• a: action (τ, ch!, ch?)
• r: reset set
• l': 도착 location

3-2. Time Transition

sl ─ec→ sl'

• sl, sl': 같은 원래 location에서 파생된 sub-location
• ec: enabling condition (예: x == n, x > n)

3-3. Sub-location 메타 정보

각 sub-location sl은 다음 정보를 가진다.

• location(sl): 원래 location
• clock(sl): 이 sub-location을 지배하는 clock
• interval(sl): 머무를 수 있는 시간 구간 (예: interval(Low_1) = (5,60))

---

4. TADA 의미론 (Semantics)

TADA의 의미론은 Labeled Transition System(LTS)으로 정의된다 (Definition 3). 상태는 다음과 같은 쌍이다.

State = (sl, v)

• sl: sub-location
• v: clock valuation
• v(clock(sl))는 반드시 interval(sl) 안에 있어야 한다.

4-1. 액션 전이 (Action Transition Rule)

(sl, v) ─a→ (sl', v')

• sl'는 action의 target location에 속하는 sub-location
• v' = v[r] (reset 수행)
• v'가 interval(sl') 안에 있어야 함

4-2. 시간 진행 (Time Progression Rule)

(sl, v) ─d→ (sl, v + d)

• d > 0 동안 interval(sl) 조건이 유지되면 언제든 시간은 흐를 수 있음
• TA의 시간 진행 semantics를 보존

4-3. 시간 경계 전이 (Time Boundary Transition Rule)

(sl, v) ─d→ (sl', v')   (0 < d < ε)

• ec = x > n인 경우: v(x) = n일 때 전이가 발생하고, v'(x) = n + d
• ec = x == n인 경우: v(x) + d = n이 되는 순간 전이가 발생

이를 통해 TA에서 암묵적이던 "x가 정확히 n이 되는 순간"을 정밀하게 모델링할 수 있다.

---

5. TADA의 장점 (TA 대비)

TA	TADA
시간 진행이 암묵적	시간 진행이 sub-location 전이로 명시화
invariant & guard가 섞여 있음	시간 조건과 행동 조건을 완전히 분리
invariant 위반을 코드에서 감지하기 어려움	violation sub-location 자동 생성
x == n을 정확한 시점에서 처리하기 어려움	각 경계값을 sub-location으로 구조화
코드 생성 시 의미적 모호성	코드 생성이 직접적이고 deterministic

TADA는 결국 시간 모델을 정규화(normalization)하여 Go 코드로의 자동 변환을 가능하게 만드는 핵심 매개체이다.

---

6. 코드 생성(Go Translation) 관점에서 TADA의 의의

TADA를 거치면 다음과 같은 변환이 매우 단순해진다.

TADA	Go Code
sub-location	Go label 블록
time transition (x == n)	<- time.After(n*T - cur - ε)
time transition (x > n)	<- time.After(n*T - cur)
action transition (ch?)	<- ch
action transition (ch!)	ch <- true
reset r	x = time.Now()

즉, TADA의 구조가 곧 Go 코드의 구조가 된다. 논문에서 제시한 파이프라인은 TA → TADA → Go로 자연스럽게 매핑되며, 최종적으로 시간 불변식 모니터링까지 자동 내장된다.

---

7. 결론: 코드 생성 수준까지 의미를 보존하는 정규화된 중간 모델

TADA는 다음을 동시에 만족하는 형식 모델이다.

• TA의 의미와 trace equivalence 유지
• 시간 경계 조건 및 invariant를 명시적으로 모델링
• action과 time을 완전히 분리
• violation state를 통해 런타임 모니터 가능
• CSP 스타일 Go 코드와 매끄럽게 매핑

즉, TA의 수학적 모델을 실제 실행 가능한 코드로 안전하게 변환하기 위한 최적의 중간 표현(IR)이다.