ISSN 2383-6318(Print) / ISSN 2383-6326(Online) KIISE Transactions on Computing Practices, Vol. 21, No. 2, pp. 132-137, 2015. 2 http://dx.doi.org/10.5626/ktcp.2015.21.2.132 타임드오토마타모델기반테스팅기법분석및사례연구 (Analysis of Timed Automata Model-based Testing Approaches and Case Study) 김한석 지은경 배두환 (Hanseok Kim) (Eunkyoung Jee) (Doo-Hwan Bae) 요약실시간시스템은시스템의행동이입력값뿐만이아니라입력값의시간에도의존적인시스템이고, 타임드오토마타는실시간시스템모델링및분석에대표적으로쓰이는모델이다. 모델기반테스팅은소프트웨어의요구사항을표현한모델로부터생성된테스트케이스를테스트대상프로그램에수행함으로써테스트대상프로그램이모델에명세된대로작동하는지여부를확인하는기법이다. 본연구에서는타임드오토마타모델기반테스팅도구인 UPPAAL-TRON, UPPAAL-COVER, SYMBOLRT 를동일한시스템에적용하는사례연구를수행하고, 이를기반으로테스팅기법및도구를비교분석한다. 키워드 : 타임드오토마타, 테스팅기법분석, 실시간시스템테스팅, 모델기반테스팅 Abstract A real-time system is a system wherein the behavior of the system depends not only on the input but also on the timing of the input. Timed automata is a widely used model for real-time system modeling and analysis. Model-based testing is employed to check whether the system under test (SUT) works according to the model specifications by using test cases generated from models that represent software requirements. In this paper, a case study was performed applying the timed automata based testing tools, UPPAAL-TRON, UPPAAL-COVER and SYMBOLRT, to the same system. Comparison of the testing approaches and tools is then made based on the results of the case study. Keywords: timed automata, testing approaches analysis, real-time system testing, model-based testing 본연구는미래창조과학부및한국산업기술평가관리원의산업융합원천기술개발사업의일환으로수행하였으며 [10044457, 자율지능형지식 / 기기협업프레임워크기술개발 ], 또한 2013 년도정부 ( 교육부 ) 의재원으로한국연구재단의지원을받아수행된기초연구사업임 (No. NRF-2013R1A1A2058618) 이논문은 2014 한국컴퓨터종합학술대회에서 타임드오토마타모델기반테스팅기법분석 의제목으로발표된논문을확장한것임 학생회원 : KAIST 전산학과 hskim@se.kaist.ac.kr 종신회원 : KAIST 전산학과교수 (KAIST) ekjee@se.kaist.ac.kr bae@se.kaist.ac.kr (Corresponding author 임 ) 논문접수 : 2014년 9월 11일 (Received 11 September 2014) 논문수정 : 2014년 11월 12일 (Revised 12 November 2014) 심사완료 : 2014년 11월 19일 (Accepted 19 November 2014) CopyrightC2015 한국정보과학회ː 개인목적이나교육목적인경우, 이저작물의전체또는일부에대한복사본혹은디지털사본의제작을허가합니다. 이때, 사본은상업적수단으로사용할수없으며첫페이지에본문구와출처를반드시명시해야합니다. 이외의목적으로복제, 배포, 출판, 전송등모든유형의사용행위를하는경우에대하여는사전에허가를얻고비용을지불해야합니다. 정보과학회컴퓨팅의실제논문지제21권제2호 (2015. 2)
타임드오토마타모델기반테스팅기법분석및사례연구 133 1. 서론 실시간시스템은시스템의행동이입력값뿐만이아니라입력값의시간에도의존적인시스템이다. 이러한시스템을테스트하기위해서는시스템에어떤입력값이제공되는지도중요하지만, 이러한입력값들이언제제공되는가도고려되어야한다 [1]. 타임드오토마타 (Timed Automata)[2] 는시간제약성을가지는실시간시스템모델링및분석에가장널리쓰이는모델중하나로, 기존의오토마타에더하여클락 (Clock) 을이용하여시간의흐름을모델링한다. 모델기반테스팅 (Model-Based Testing) 은소프트웨어요구사항을표현한모델로부터생성된테스트케이스를, 테스트대상프로그램에수행하여테스트대상프로그램이모델에명세된대로작동하는지여부를확인하는기법이다 [3]. 본연구에서는대표적인타임드오토마타모델기반테스팅도구 [4] 로서, 테스트생성과실행을동시에하는 UPPAAL- TRON 도구 [5], 테스트커버리지기준 (Test Coverage Criteria) 을충족하는테스트케이스를자동으로생성하는 UPPAAL- COVER 도구 [6], 테스트목적 (Test Purpose) 을이용해서테스트케이스를생성하는 SYMBOLRT 도구 [7] 를동일한시스템에적용하는사례연구를수행하고, 이를기반으로테스팅기법및도구를비교분석한다. 본논문의구성은다음과같다. 2장에서 UPPAAL- TRON 도구, UPPAAL-COVER 도구, SYMBOLRT 도구를소개하고, 3장에서는이들도구에대한비교분석과사례연구를기반으로주요이슈사항을도출한다. 4장에서는결론및향후연구를기술한다. 2. 타임드오토마타모델기반테스팅기법소개 2.1 대상모델그림 1[8] 은여러열차들의접근을제어하는타임드오토마타모델이다. 한번에하나의열차만통과할수있도록제어를하는것이목적이며, 기존열차가없는상태에서한열차가접근을하면서접근하고있다는신호 (appr) 를보내면, 초기상태인 Free에서 Occ로상태가변경되면서, 해당열차의 ID가큐에저장이된다. 이때다른열차가접근하면, 해당열차의 ID를큐에저장함과동시에현재지나가고있는열차가통과할때까지멈추라는신호 (stop) 를보내게되며, 기존의열차가떠난다는신호 (leave) 를보내어 Occ에서 Free로상태가변경이되면, 큐의내용을검사해서기존에멈춰있는열차들에게순차적으로출발하라는신호 (go) 를보내거나, 큐가비어있는경우다시새로운열차를기다리게된다. 그림 1 열차제어장치모델 [8] Fig. 1 Train controller model [8] 그림 2 열차환경모델 [8] Fig. 2 Train environment model [8] 그림 2[8] 는열차제어장치모델을이용하는열차들을모델링한환경오토마타이다. 열차가안전한상태 (Safe) 에서플랫폼으로접근하고있는상태 (Appr), 다른열차가통과할때까지기다리는상태 (Stop), 다시출발하는상태 (Start), 통과하고있는상태 (Cross) 로구성되어있으며, 열차들의통과시간을제어하기위해클락값을사용하였고, 각열차구분을위해열차번호 (id) 를명명하였다. 그림 1과 2의모델을예제로각도구에적용하였다. 2.2 UPPAAL-TRON 도구 UPPAAL-TRON 도구는테스트생성과실행을동시에수행하는온라인테스팅도구로서 [5], UPPAAL 모델 [8] 로기술된시스템의모델에서수행되는값을 UPPAAL-TRON 엔진과어댑터를거쳐서테스트대상시스템 (SUT) 으로보내직접테스트를수행하고, 테스트결과값을다시어댑터와 UPPAAL-TRON 엔진을통해실제모델의값과비교하여테스트의성공또는실패여부를결정한다.
134 정보과학회컴퓨팅의실제논문지제 21 권제 2 호 (2015.2) 그림 3 UPPAAL-TRON 도구에서의테스트수행결과 Fig. 3 Test result using the UPPAAL-TRON tool 온라인테스팅도구로서 SUT와직접교신하는방식을택한 UPPAAL-TRON 도구는모델을테스트하는동안특정테스트커버리지기준에의존하지않고, 시스템명세에포함된상태들을확률적선택기법을이용하여생성할테스트를제한한다 [9]. 그림 3은 UPPAAL-TRON 도구를사용하여그림 1 의열차제어장치모델을테스트한결과이다. 변수값 4( 열차번호 4) 를가진 appr이라는신호가온뒤에, 변수값 1( 열차번호 1) 을가진 appr이라는신호가오면, 바로 stop이라는신호로열차를정지시키는테스트수행과정을확인하였으며, 정해진테스팅시간이지난후에, 테스팅하는동안결함을가진행위가발견되지않았음을알려주는 TEST PASSED 메시지와함께테스트가종료되었다. 2.3 UPPAAL-COVER 도구 UPPAAL-COVER 도구는 UPPAAL 모델로기술된타임드오토마타로부터테스트커버리지기준을충족하는테스트케이스를자동으로생성하는도구로서 [6], UPPAAL 도구로모델링된모델과테스트커버리지기준이저장되어있는옵저버 (Observer), 옵저버이름을명시한쿼리 (Query) 파일을 UPPAAL-COVER 도구에입력하여옵저버에명시된테스트커버리지기준에부합되는테스트케이스를자동으로생성한다. 시스템명세로부터확률적선택기법을이용하여테스트케이스를생성하는 UPPAAL-TRON 도구와는다르게, UPPAAL-COVER 도구는특정테스트커버리지기준을충족하는테스트케이스를생성하는특징이있다. 그림 4(a) 는열차제어장치모델을대상으로 All-Node 커버리지기준 ( 모델의모든 Node를한번이상커버하는 테스트케이스를생성하는커버리지기준 ) 을만족하는테스트케이스를생성한결과이다. 2.4 SYMBOLRT 도구 SYMBOLRT 도구는타임드입출력심볼릭전이시스템 (Timed Input-Output Symbolic Transition System: TIOSTS) 모델을기반으로한모델기반테스팅도구로서 [7], 테스트대상모델에특화된테스트목적을테스터가 TIOSTS 모델과함께 SYMBOLRT 도구에입력하여테스트케이스를자동으로생성한다. UPPAAL-COVER 도구와는다르게테스트커버리지를옵저버를이용하여명세하지않고, 테스트대상모델에명시적으로테스트목적을작성하여수행함으로써테스트커버리지를충족하는테스트케이스를생성하는특징이있으며, 그림 4(b) 는그림 1의모델과함께모델의모든노드를커버하는테스트목적을가지고생성한테스트로, 열차한대접근후다른열차가접근하면멈추라는신호를보내는테스트시퀀스를나타낸다. SYM- BOLRT 도구는생성된테스트케이스의시각적표현을지원한다. 3. 타임드오토마타모델기반테스팅도구비교분석 3.1 사례연구그림 1의열차제어장치모델을사례연구의대상모델로선정하였으며, 이를각모델기반테스팅도구들을이용해서테스팅을수행함으로써타임드오토마타모델기반테스팅도구들을비교분석하고테스팅이슈를제안하였다. 사례연구및비교분석을위해 UPPAAL-TRON 도구와 UPPAAL-COVER 도구에입력파일로들어갈 UPPAAL 모델 [8] 을준비하였고, 이와동일한모델을 TIOSTS 모델 [7] 로변환하여 SYMBOLRT 도구의입력파일로사용하였다. 준비된모델외에추가적인작업으로 UPPAAL-TRON 도구는테스트대상시스템 (SUT) 을실제로구현하였으며, UPPAAL-COVER 도구는테스트커버리지기준을옵저버와쿼리파일로준비하였다. SYMBOLRT 도구는 UPPAAL-COVER 도구에서사용한테스트커버리지기준과동일한내용의테스트목적을 TIOSTS 모델로변환하여사용하였다. 3.2 테스팅결과동일한모델을각도구에서수행한결과는그림 3과그림 4(a), 4(b) 와같았다. 2장에서설명한것과같이, 열차한대가통과하고있을때, 다른열차가접근하면해당열차를멈추는일련의과정을각모델기반테스팅도구에서동일하게볼수있었으며, 이러한테스팅결과와각테스팅도구의특징을비교하기위해 [10] 의연구결과로도출된그림 5의분류기준들을활용하였다.
타임드 오토마타 모델 기반 테스팅 기법 분석 및 사례 연구 135 각 분류기준들은 모델 기반 테스팅 기법들을 모델의 명세, 특징부터 테스트를 실행하는 방식 등 총 6개의 항 목으로 구성되어 있으며, 세부적으로는 3개의 모델 명세 항목과 2개의 테스트 생성 항목, 1개의 테스트 실행 항 목으로 구성된다. 본 논문에서는 이러한 비교 항목들과 함께 테스팅 도구의 비교를 위하여 1개의 사용 편의성 (Usability) 항목을 추가하였으며, 이는 표 1과 같이 정 리하였다. 우선, [10]의 연구에서 모델 기반 테스팅 도구들의 분 류체계로 기술한 모델 명세 측면에서는 3개의 테스팅 도구가 모델 내 SUT의 입/출력을 명세하고, 시스템 모 델이 타임드 모델이면서 비결정적, 연속적인 전이 기반 모델이라는 점에서 공통점이 존재하였으나, 테스트 생성 과 실행 관점에서는 다음과 같은 차이점이 존재하였다. 테스트 선택 기준 측면에서는 UPPAAL-TRON 도구 는 시스템 명세에 포함된 상태들을 확률적으로 선택하 는 임의/확률적 선택 기법으로 테스트를 선택하였으나, UPPAAL-COVER 도구는 All-Node 커버리지 기준과 같은 구조적 모델 커버리지로 테스트를 선택하였으며, SYMBOLRT 도구는 요구사항 기반으로 명시된 테스트 목적을 커버리지로 테스트를 선택하였다. 테스트 생성 기술 측면에서는 UPPAAL-TRON 도구 는 확률적으로 선택된 테스트를 임의 실행하였으나, UPPAAL-COVER 도구는 노드 커버리지 알고리즘과 같은 검색 알고리즘을 이용하여 테스트를 생성하였고, SYMBOLRT 도구는 TIOSTS 모델에서 생성된 테스트 를 심볼릭 실행함으로써 테스트를 생성하였다. 마지막 테스트 실행 측면에서 UPPAAL-TRON 도구는 테스트 의 생성과 실행을 동시에 수행하는 온라인 테스팅 도구 였으나, 다른 도구들은 테스트의 자동 생성만 수행하는 오프라인 테스팅을 수행하였다. 이 외에도 각 모델 기반 테스팅 도구를 활용한 결과 편이성 측면에서 UPPAAL-TRON 도구는 온라인 테스 팅으로서 테스트 수행결과를 즉시 확인할 수 있다는 특 징이 있었으며, UPPAAL-COVER 도구는 테스트 커버 리지 기준이 옵저버에 잘 구현되어 있으면, 입력 값으로 주어지는 어느 모델에도 테스트 케이스가 쉽게 생성이 가능한 장점이 있었다. SYMBOLRT 도구는 각 테스트 케이스를 다른 도구들보다 시각적으로 보여줌으로써 사 용의 편의성을 높였다. 3.3 타임드 오토마타 모델 기반 테스팅 기법 관련 이슈 동일한 시스템의 모델을 다른 특징을 가지고 있는 세 가지 타임드 오토마타 모델 기반 테스팅 도구들에 적용 (a) UPPAAL-COVER (b) SYMBOLRT 을 한 결과 몇 가지 제약사항을 발견하였다. 그림 4 열차 제어장치 모델의 테스트 케이스 본 연구의 대상모델인 그림 1의 열차 제어장치 모델은 Fig. 4 Test case of the train controller model 그림 2의 열차 환경 모델과 연동하여 수행이 되며, 여러
136 정보과학회컴퓨팅의실제논문지제 21 권제 2 호 (2015.2) 그림 5 모델기반테스팅기법분류 [10] Fig. 5 The taxonomy of model-based testing approaches [10] Model Specification Test Generation Test Execution Tool Characteristics 표 1 타임드오토마타모델기반테스팅도구비교 Table 1 Comparison of the timed automata model-based testing tools Scope Characteristics Paradigm UPPAAL-TRON[5] UPPAAL-COVER[6] SYMBOLRT[7] Input-output Timed / Non-Deterministic / Continuous Transition-Based Test Selection Criteria Random and Stochastic Structural Model Coverage Requirements Coverage Technology Random generation Search-based algorithms Symbolic execution On/Offline Online Offline Usability Immediate test execution results available Easy application to various models Visual results provided 열차의운행을모델링하기위하여내부적으로는여러개의환경모델이존재하는것처럼동작한다. UPPAAL- TRON 도구와 UPPAAL-COVER 도구는이러한여러모델들을테스팅하는것에문제가없었던반면에, SYMBOLRT 도구를이용한경우에는모든모델들을하나의프로세스 (Process) 로통합하는과정에서제약사항이발생하였으며, 이는본연구에서사용한것보다복잡한모델을사용하는경우, 모델을만드는것자체에확장성 (Scalability) 문제가발생할가능성이있다. 모델자체의확장성문제와함께고려할사항으로테스트커버리지적용에있어서의확장성문제도있다. SYMBOLRT 도구는대상모델파일안에테스트커버리지를테스트목적이라는프로세스로같이명시하게된 다. 즉, 대상모델프로세스와테스트목적프로세스로구성된파일을이용하여테스트를수행하게된다. 이렇게작성되는테스트목적은시스템의요구사항을기반으로작성되기때문에복잡한시스템을모델링하는경우, 확률적으로테스트를선택하는 UPPAAL-TRON 도구나구조적테스트커버리지기준을활용하는 UPPAAL-COVER 도구와는다르게또다른확장성문제를가질가능성이있다. 이와같은확장성문제를고려한결과, 보다시각적으로테스트를보여주고관리가가능한 SYMBOLRT 도구의장점을기반으로대상모델과테스트커버리지기준의확장성제약이보다유연한 UPPAAL-COVER 도구의장점등을병행하여연구하고이러한기법들을동시에적용하는방안을강구하는것이필요할것이다.
타임드오토마타모델기반테스팅기법분석및사례연구 137 4. 결론및향후연구 본논문에서는실시간시스템을위한타임드오토마타모델기반테스팅도구인 UPPAAL-TRON 도구, UPPAAL-COVER 도구, SYMBOLRT 도구를열차제어장치모델에적용하여사례연구를수행하였다. 이를기반으로타임드오토마타모델기반테스팅기법들을비교분석하여, 몇가지관련이슈사항들을도출하였으며특히, 동일모델을각테스팅도구들에적용함으로써보다객관적인비교분석결과를얻을수있었다는점에서의미가있다. 향후연구에서는본연구에서확인한이슈들을해결하는방안을포함하여, 기존타임드오토마타모델기반테스팅기법들을개선하는연구를수행하고자한다. References [1] A. Hessel, "Model-based test case generation for real-time systems," Ph.D, Dissertation, U ppsala University, Sweden, May. 2007. [2] R. Alur, "Timed automata," Verification of Digital and Hybrid Systems, Vol. 170, pp. 233-264, Springer Berlin Heidelberg, 2000. [3] A. Pretschner, W. Prenninger, S. Wagner, C. Kühnel, M. Baumgartner, B. Sostawa, R. Zolch, T. Stauner, "One evaluation of model-based testing and its automation," Proc. of the 27th international conference on Software engineering, pp. 392-401, May. 2005. [4] M. T. B. Waez, J. Dingel, and K. Rudie, "A survey of timed automata for the development of real-time systems," Computer Science Review, Vol. 9, pp. 1-26, Aug. 2013. [5] K.G. Larsen, M. Mikucionis, B. Nielsen, and A. Skou, "Testing real-time embedded software using UPPAAL-TRON: an industrial case study," Proc. of the 5th ACM international conference on Embedded software, pp. 299-306, Sep. 2005. [6] A. Hessel, and P. Pettersson, "CoVer-a real-time test case generation tool," Proc. of the 19th IFIP International Conference on Testing of Communicating Systems and 7th International Workshop on Formal Approaches to Testing of Software, 2007. [7] W. L. Andrade, and P. D. L. Machado, "Generating Test Cases for Real-Time Systems Based on Symbolic Models," IEEE Transactions on Software Engineering, Vol. 39, No. 9, pp. 1216-1229, Sep. 2013. [8] G. Behrmann, A. David, and K. G. Larsen, "A Tutorial on UPPAAL 4.0," Department of Computer Science, Aalborg University, Denmark, 2006. [9] A. Hessel, K.G. Larsen, M. Mikucionis, B. Nielsen, P. Pettersson, and A. Skou, "Testing real-time systems using UPPAAL," Formal methods and testing, Vol. 4949, pp. 77-117, Springer Berlin Heidelberg, 2008. [10] M. Utting, A. Pretschner, and B. Legeard, "A taxonomy of model-based testing approaches," Software Testing, Verification and Reliability, Vol. 22, No. 5, pp. 297-312, Aug. 2012. 김한석 2003년숭실대학교컴퓨터학부학사. 2004 년~2006년육군본부정보체계관리단장비정비개발실담당. 2009년 Air Force Institute of Technology (AFIT) 전산학과석사. 2010년~2012년방위사업청종합군수지원개발1팀담당. 2012년~현재 KAIST 전산학과박사과정. 관심분야는소프트웨어공학, 모델검증, 모델기반테스팅, 소프트웨어보안 지은경 1999 년 KAIST 전산학과학사. 2001 년 KAIST 전산학과석사. 2001 년 ~2002 년몽골울란바타르대학전임강사. 2003 년 ~2004 년 ( 주 ) 이마린로직스소프트웨어엔지니어. 2009 년 KAIST 전산학과박사. 2009 년 ~2011 년 University of Pennsylvania 박사후연구원. 2011 년 ~ 현재 KAIST 전산학과연구조교수. 관심분야는소프트웨어공학, 소프트웨어테스팅, 정형검증, 안전필수소프트웨어, 소프트웨어안전성 배두환 1980년서울대학교조선공학학사. 1987 년 Univ. of Wisconsin-Milwaukee 전산학과석사. 1992년 Univ. Of Florida 전산학과박사. 1995년~현재 KAIST 전산학과교수. 관심분야는소프트웨어프로세스, 객체지향프로그래밍, 컴포넌트기반프로그래밍, 임베디드소프트웨어설계, 관점지향프로그래밍