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

TA–TADA–to–Go: Ensuring CPS Reliability

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