Skip to main content

UPPAAL 시뮬레이션 트레이스를 이용한 시간 모델의 가상 프로토타입 기반 시뮬레이션

· 4 min read
김지훈
박흥준
이우진
담당교수

논문 정보​

  • 제목: Virtual Prototype Based Simulation of Timed Model for UPPAALL Simulation Trace
  • 저자: 김지훈, 박흥준, 이우진 (경북대학교 융합소프트웨어학과/컴퓨터학부)
  • 학회/저널: 2014년 한국컴퓨터종합학술대회 논문집 (KCC 2014)
  • 발행일: 2014-06-25
  • 주요 연구 내용: 실시간 시스템 검증 도구인 UPPAAL의 시뮬레이션 트레이스 파일을 파싱하여, Flash 기반의 가상 프로토타입(VP)과 연동함으로써 모델의 동작을 시각적으로 시뮬레이션하는 기법을 제안한다.
  • 주요 결과 및 결론: Infusion Pump 예제를 통해 텍스트 형태의 난해한 UPPAAL 시뮬레이션 결과를 실제 장치의 동작처럼 가시화하여 표현함으로써, 개발자가 모델의 동작과 시간 제약 조건을 직관적으로 이해하고 확신을 가질 수 있음을 보였다.
  • 기여점: 기존 UPPAAL 시뮬레이터의 텍스트 출력 한계를 극복하고, 하드웨어 없이도 시간 제약이 포함된 임베디드 시스템 모델의 동작을 시각적으로 검증할 수 있는 환경을 구축했다.

요약​

초록​

UPPAAL은 Timed Automata 기반의 실시간 시스템 검증 도구로 널리 사용되지만, 그 시뮬레이션 결과가 단순 텍스트 형태로 제공되어 모델의 동작을 직관적으로 이해하기 어렵다. 본 논문은 이러한 문제를 해결하기 위해 UPPAAL의 시뮬레이션 결과를 UTAP(Uppaal Timed Automata Parser)를 통해 분석하고, 이를 가상 프로토타입(Virtual Prototype, VP)과 연결하는 방법을 제안한다. 이를 통해 시간 제약 조건을 만족하는 높은 시각적 효과의 시뮬레이션 결과를 제공하여 모델에 대한 이해도와 신뢰성을 높인다.

서론​

임베디드 시스템의 기능이 복잡해짐에 따라 소프트웨어 검증이 중요해지고 있다. 하지만 하드웨어 제약으로 인해 개발 및 테스트가 어렵다는 문제가 있다. 이를 해결하기 위해 디지털 Mock-Up이라 불리는 가상 프로토타입(VP)을 이용한 시뮬레이션이 활용된다. 본 연구는 UPPAAL 시뮬레이션 트레이스 정보를 추출하여 VP가 동작해야 하는 신호를 시간 제약에 맞춰 전송함으로써, 개발자가 모델의 동작을 가시적으로 확인할 수 있도록 한다.

배경​

UPPAAL은 실시간 시스템 모델링 및 검증 도구로, 시스템 동작을 설명하는 기술 언어, 시뮬레이터, 모델 체커로 구성된다. 시뮬레이터는 모델의 동적 실행을 가능하게 하지만 결과가 텍스트 위주이다. 한편, SWF(Shockwave Flash) 기반의 VP는 임베디드 시스템의 장치를 컴포넌트 단위로 가시화하여 시각적 요소들이 결합된 시스템 이미지를 제공한다. 본 연구는 이 두 가지 요소를 결합하여 시뮬레이션 기법을 연구한다. Figure 1 Figure 2

모델 아키텍처 / 방법론​

  • 핵심 구조: 논문의 Figure 1에서 제시된 전체 구조는 Model.xml, Trace.xtr, Model.if 파일을 기반으로 한다. xtr 파일과 if 파일에서 추출한 정보는 Trace Info Manager에서 관리되며, 이는 VP State Manager와 연동되어 System Image를 제어한다.
  • 트레이스 파싱: UPPAAL의 verifyta.exe를 통해 생성된 중간 포맷(if)과 트레이스 파일(xtr)을 UTAP 라이브러리를 사용하여 파싱한다. 트레이스 순서는 State -> Act -> State... 형태로 표현되며, 각 상태의 제약 시간 정보와 다음 상태로 넘어가기 위한 메시지 정보를 추출하여 배열에 저장한다.
  • 시뮬레이션 진행: Figure 2의 순서도와 같이 시뮬레이션은 시간 제약에 맞게 진행된다. 상태 진입 시점과 메시지 처리 시점의 차이를 계산하여 제약 시간을 만족할 때 Output 메시지를 발생시킨다.
  • 메시지 테이블: VP State Manager는 컴포넌트 상태 테이블과 컨트롤 테이블을 참조하여 System Image의 상태를 제어한다. 테이블은 Component, StateName, TransitionString 등으로 구성되어 VP의 시각적 상태(act/deact)를 결정한다. Figure 3 Figure 4, 5

실험 결과​

  • 적용 예제: 본 논문은 환자에게 약물을 주사하는 Infusion Pump 모델을 대상으로 시뮬레이션을 구현했다(Figure 3).
  • 모델 동작:
    • Start 상태에서 BolusReq? 메시지를 받으면 BolusRequested 상태로 진입한다.
    • 진입 후 시간 제약 x≤5x \le 5 내에서 동작하며, 3초에서 5초 사이에 StartInfusion! 메시지를 발생시킨다.
    • 이후 Infusion 상태(x≤10x \le 10)로 전이된다.
  • 시각화 결과: Figure 4의 콘솔 창과 Figure 5의 VP 이미지를 통해 결과를 확인했다. 단순히 텍스트로 State 이동만 보여주는 기존 방식과 달리, VP 연동 시뮬레이션은 현재 상태에 따라 펌프의 이미지와 디스플레이가 변경되는 것을 가시적으로 보여주었다. 예를 들어, Infusion 상태나 Alarming 상태에 따라 VP의 그래픽이 해당 동작을 묘사하도록 변경된다.

결론​

본 논문은 UPPAAL 시뮬레이터의 결과가 단순 문자로 나타나는 한계를 극복하기 위해 SWF 기반 VP를 이용하는 방법을 제안했다. 트레이스 파일로부터 정보를 추출하여 VP와 연동함으로써 시뮬레이션 결과를 직관적으로 확인할 수 있게 되었다. 향후 연구로는 실제 제작된 소프트웨어와 UPPAAL 모델 시뮬레이션 결과를 동시에 VP에 연결하여, 소프트웨어와 모델을 교차 검증하는 방법에 대해 연구할 계획이다.