형식 검증 기반 CPS 신뢰성 확보: TA–TADA–to–Go 프레임워크

본 연구는 자율주행, 산업 자동화 등과 같은 안전 필수(Critical) 사이버-물리 시스템(CPS)에서 요구되는 정확성·안전성·시간적 제약 준수를 보장하기 위한 새로운 통합 접근법을 제안한다. 기존 Timed Automata(TA) 및 UPPAAL 기반 오프라인 형식 검증은 이론적으로 강력하지만, 이를 실제 실행 가능한 코드로 변환하는 과정에서 의미 손실이 발생하거나, 레거시 ROS 시스템·센서 지연·스케줄링 변동으로 인해 런타임 위반이 발생할 위험이 남아 있다.

이를 해결하기 위해 본 연구는 그림과 같이 형식 검증(Verification) → TADA 기반 자동 코드 생성(Implementation) → Go 실행 및 런타임 모니터링(Execution)으로 이어지는 3단계 파이프라인 TA–TADA–to–Go를 제안한다.

---

1. 형식 검증 단계: Timed Automata 기반 안전성 검증

첫 단계에서는 UPPAAL을 사용해 CPS의 안전 필수 컴포넌트를 Timed Automata로 모델링하고, Timed-CTL 기반 속성 검증을 수행한다.

• 시간 제약을 포함한 소프트웨어 요구사항, 환경 모델, 상호작용 구조를 TA로 모델링
• 안전성(safety), 도달성(reachability), 응답성(bounded response) 등의 속성을 Timed-CTL로 명세
• 모델 체킹을 통해 시간적 무결성 및 논리적 안전성을 사전에 보장

---

2. TADA 기반 자동 코드 생성: 의미를 잃지 않는 중간 표현

TA 모델을 직접 코드로 변환하면 시간 의미(semantics)가 모호해지기 쉽다. 이를 해소하기 위해 본 연구는 새로운 형식 모델인 TADA (Timed Automata with Disjoint Actions)를 도입한다.

• 각 TA 위치(location)를 여러 개의 sub-location으로 분해하여 시간 흐름(time progression)을 명시적으로 표현
• 시간 전이(time transition)와 동작 전이(action transition)를 분리해 실행 타이밍의 비결정성을 제거하고 구현 용이성을 확보
• x == n, x > n 등 시간 경계 조건을 명시적으로 모델링하여 Go의 select 문, time.After()와 자연스럽게 매핑
• 원래 TA와 추적(trace) 동등성을 유지하여, UPPAAL에서 검증된 의미를 손실 없이 실행 코드 수준으로 전달

이 과정을 통해 TA → TADA → Go로 이어지는 완전 자동화 코드 생성 파이프라인을 구축하였다.

---

3. 실행 단계: Go 기반 실행 및 런타임 시간제약 모니터링

TADA로부터 생성된 Go 코드는 다음 두 가지 구성 요소를 포함한다.

3-1. 기능적 소프트웨어 코드 (Behavior Code)

• 각 (sub-)location을 Go의 라벨(label) 블록으로 구현하고 goto를 이용해 전이 구현
• goroutine과 channel을 활용하여 TA/TADA의 병렬 실행 semantics를 CSP 스타일로 충실히 구현
• time.Now(), time.Since(), time.After()를 이용해 논리적 clock을 실제 시간으로 매핑

3-2. 내장 런타임 모니터 (Time-Invariant Monitors)

• TA/TADA에서 정의된 시간 불변식(time invariant)을 Go 코드 내부 모니터로 함께 생성
• 실행 중 x ≤ n, x == n 등의 제약 위반이 발생하면 위반 채널(violation channel)을 통해 알람 전송
• ROS, DDS, 스케줄링 지연, GC 지연 등으로 인한 실제 타이밍 문제를 런타임에서 직접 감지하고 안전 복귀(safe recovery)를 트리거

이와 같이 오프라인 형식 검증 + 온라인 모니터링을 결합함으로써, 순수 모델 검증만으로는 잡기 어려운 실행 시 타이밍 문제까지 포착할 수 있다.

---

4. 사례 연구: ROS 기반 산업 제어 시스템 적용

제안 프레임워크를 ROS 기반 산업 제어 시스템에 적용하여 다음과 같은 결과를 확인하였다.

• 레거시 노드 및 통신 지연으로 인해 발생하는 타이밍 위반을 자동 감지 및 차단
• Jetson TX2와 같은 임베디드 플랫폼에서도 모델 기반 Go 실행 환경이 실용적인 성능을 보임
• 순수 오프라인 검증 방법에 비해, 형식 검증 + 런타임 관측(hybrid approach)이 전체 시스템의 안전성·탄력성을 유의미하게 향상시킴

---

5. 본 연구의 핵심 기여

• 형식 검증에서 실제 실행 코드까지 이어지는 완전 자동화 파이프라인 (Verification → Implementation → Execution) 제시
• 시간 의미를 명확히 보존하는 중간 모델 TADA (Timed Automata with Disjoint Actions) 제안
• 정형 모델 기반 Go 코드 생성과 런타임 시간제약 모니터링을 결합한 CPS 신뢰성 강화 기법 제시
• ROS 등 레거시 환경에서 발생하는 지연·지터를 실행 시점에서 감지·대응하는 메커니즘 구현
• 실제 CPS 사례 연구를 통해 안전성 및 신뢰성 향상 효과를 정량·정성적으로 실증

---

6. 논문 인용 (Citation)

IEEE Access (2025)

Soomin Cho, Inhye Kang, and Jin Hyun Kim,
“From Timed Automata to Go: Formally Verified Code Generation and Runtime Monitoring for Cyber-Physical Systems,”
IEEE Access, vol. 13, pp. 161729–1617xx, 2025.
doi: 10.1109/ACCESS.2025.3608215
[IEEE Xplore]

HTML용 간단 표기:
Cho, S., Kang, I., & Kim, J. H. (2025). “From Timed Automata to Go: Formally Verified Code Generation and Runtime Monitoring for Cyber-Physical Systems.” IEEE Access, 13, 161729–1617xx. https://doi.org/10.1109/ACCESS.2025.3608215

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)이다.

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/변수 값을 포함하는 튜플입니다.

• 상태 = (loc₁, ..., loc_n, 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 코드와 런타임 모니터로 자동 변환됨으로써 형식 검증에서 실제 실행 환경까지 일관된 신뢰성 보증을 가능하게 합니다.