DBPIA-NURIMEDIA

Size: px

Start display at page:

Download "DBPIA-NURIMEDIA"

경심 변
7 years ago
Views:

1 안전성이중요한시간기반내장형소프트웨어의시간제약성검증에관한사례연구 647 안전성이중요한시간기반내장형소프트웨어의시간제약성검증에관한사례연구 (A Case Study on Timing Constraints Verification for Safety-Critical, Time-Triggered Embedded Software) 최진호 지은경 김현정 배두환 (Jinho Choi) (Eunkyoung Jee) (Hyeon-Jeong Kim) (Doo-Hwan Bae) 요약유도조종장치는안전성이중요한시간기반내장형시스템이며유도조종장치소프트웨어의시간제약성만족은소프트웨어안전성확보를위한매우중요한문제이다. 기존유도조종장치소프트웨어개발에서는주로테스트단계의시뮬레이션기법을통해시간제약성만족을확인한다. 하지만시뮬레이션환경을구축하기위한추가적인시간과노력이소요될뿐만아니라시간관련오류의개발후발견은소프트웨어안전성을저하시키며, 전체소프트웨어개발비용을증가시킬수있다. 이러한단점을보완하기위해본논문에서는설계단계에모델체킹기법을적용하여유도조종장치소프트웨어의시간제약성을검증하고자한다. 이를위해서실시간시스템에대한모델링과검증을지원하는 TIMES 도구를유도조종장치소프트웨어설계에적용하는사례연구를수행하고그결과를분석및평가하였다. 키워드 : 시간제약성, 모델체킹, 내장형소프트웨어설계, 실시간시스템, 유도조종장치 Abstract Guidance and Control Unit (GCU) is a safety-critical and time-triggered embedded system and it is crucial to satisfy with timing constraints of GCU software to increase software safety. Usually timing constraints of GCU software are validated with a simulation method in test phase. However, constructing simulation environments needs to invest much time and effort. Furthermore, detecting errors in later phases can lead to a development cost increase. To compensate these drawbacks, a model checking method can be applied to validate timing constraints of GCU software in design phase. To this end, we accomplish a case study on validating GCU software using TIMES model checking tool, and evaluate results of the case study. Key words : timing constraints, model checking, embedded software design, real-time system, guidance and control unit (GCU) 본연구는국방과학연구소의연구비지원으로수행하였습니다.( 과제명 : 무기체계 ( 유도조종장치용 ) 내장형 safety-critical S/W 설계기법및재사용지원시스템 종신회원 : KAIST 전산학과교수 bae@se.kaist.ac.kr 연구, 계약번호 UD100031CD) 논문접수 : 2011년 7월 11일 이논문은 2011 한국컴퓨터종합학술대회에서 안전성이중요한실시간시스템의 심사완료 : 2011년 9월 19일 시간제약성검증에관한사례연구 의제목으로발표된논문을확장한것임 학생회원 : KAIST 전산학과, 국방과학연구소 jhchoi@se.kaist.ac.kr 종신회원 : KAIST 전산학과교수 ekjee@se.kaist.ac.kr 학생회원 : KAIST 전산학과 hjkim@se.kaist.ac.kr CopyrightC2011 한국정보과학회ː개인목적이나교육목적인경우, 이저작물의전체또는일부에대한복사본혹은디지털사본의제작을허가합니다. 이때, 사본은상업적수단으로사용할수없으며첫페이지에본문구와출처를반드시명시해야합니다. 이외의목적으로복제, 배포, 출판, 전송등모든유형의사용행위를하는경우에대하여는사전에허가를얻고비용을지불해야합니다. 정보과학회논문지 : 소프트웨어및응용제38권제12호 ( )

2 648 정보과학회논문지 : 소프트웨어및응용제 38 권제 12 호 ( ) 1. 서론실시간내장형시스템개발에서소프트웨어의시간제약성을분석하고검증하는작업은매우중요하다 [1,2]. 국방분야의유도조종장치는대표적인실시간내장형시스템으로유도조종장치소프트웨어개발에서전체비행시스템을테스트하는비행시험전에유도조종장치소프트웨어의태스크행위명세 (task behavior specification)[3] 와스케줄링등시간제약성에문제가없는지분석하고확인하는일은안전성확보에필수적이다. 시간과관련된사소한소프트웨어에러로인해서고가의비행시스템의임무수행이실패로끝날수있으며, 최악의경우에는사고로인해예기치않은인적, 물적피해를입을수있기때문이다. 유도조종장치소프트웨어의시간제약성확인은일반적으로테스트단계에서시뮬레이션기법을통해이루어진다 [4]. 다른실시간내장형소프트웨어와마찬가지로유도조종장치내장형소프트웨어의시간제약성을테스트하는데는많은시간과노력이요구된다. 유도조종장치소프트웨어의테스트를위해서는기본적으로호스트장비에서구현된코드를실행가능한파일로변환하고, 타켓장비인유도조종장치와의연결을통해실행파일을탑재하는일련의작업이수행된다. 또한시뮬레이션을위해서는유도조종장치뿐만아니라시뮬레이션구동장비, 테스트데이터저장장비등다수의시뮬레이션지원장비가필요하며태스크스케줄링을정확하게분석하기위해오실로스코프나로직애널라이저등의장비를이용해서유도조종장치소프트웨어에서출력되는스케줄링관련신호를확인하기도한다. 하지만시뮬레이션기법은소프트웨어의부분적인실행경로에대한수행가능성만을확인할수있으며, 시뮬레이션을수행하기위한테스트환경이먼저구축되어야하는단점이있다. 이러한테스트작업들은유도조종장치소프트웨어구현이후에이루어지기때문에요구사항과설계단계에서발생되어잠재된시간관련소프트웨어오류의발견이늦어지게되어전체소프트웨어개발비용을증가시킬수있다. 이러한문제점을개선하기위해구현이후단계가아닌요구사항분석및설계단계에서부터시간제약성검증을수행하여유도조종장치소프트웨어의안전성을높이는것이중요하다. 모델체킹기법을사용하면대상소프트웨어에대한모델이사용자가정의한속성을만족하는지를자동으로검증할수있으며, 특히실시간모델체커를이용하면시간제약성검증이가능하다 [5]. 또한모델체킹기법은시뮬레이션에비해전체소프트웨어모델의행위를검증할수있는장점을가진다 [5,6]. 본논문에서는실제국방도메인에서사용되는유도조종장치내장형소프트웨어설계에서모델체킹기법이어떻게유용하게사용될수있는지분석하고적용가능성을확인하고자한다. 이를위해서실시간시스템을모델링할수있는모델체킹도구인 TIMES[7-9] 를사용하여유도조종장치소프트웨어의태스크행위명세를모델링하고검증한다. 본논문의구성은다음과같다. 2장에서는 TIMES 도구와본연구의대상시스템인유도조종장치에대해서술하고, 3장에서는유도조종장치소프트웨어요구사항분석과개념설계에대해기술한다. 4장에서는 TIMES 도구를이용해서유도조종장치타임드오토마타모델을명세하고명세모델의속성을이용한모델검증결과를보이며, 반례를통해명세모델과속성의오류를수정한과정에대해서술한다. 5장에서는본연구에대한평가를기술하며, 6장은관련연구로서 TIMES 이외의다른실시간모델체킹도구들과실시간내장형시스템의시간제약성검증에모델체킹을활용한연구에대해알아본다. 마지막으로 7장에서결론과향후연구에대해서술한다. 2. 배경 2.1 TIMES 실시간시스템의행위검증을위한실시간모델체커로는 TIMES, UPPAAL[10], PAT[11], TSMV[12], KRONOS[13] 등이있다. 이중에서 TIMES는다른모델체커들과달리태스크를가지는확장된타임드오토마타를사용하여태스크스케줄링가능성을분석할수있으며, 시간기반구조를잘표현할수있다 [9,14,15]. 따라서본논문에서는 TIMES를사용하여시간기반구조를가지는유도조종장치소프트웨어의행위를명세한다. TIMES는실시간시스템에대한모델링, 시뮬레이션, 검증, 코드생성을지원하는도구이다 [7-9]. 모델링에서는타임드오토마타를이용해서대상소프트웨어의행위를모델링하고태스크의시간제약성정보와선점, 비선점과같은스케줄링정책에대한정보를명세한다 [7,15]. 타임드오토마타는그림 1에서보는것과같이기본적으로노드와트랜지션의조합으로구성되며, 노드와트랜지션에클락변수를사용해서시간제약성을명세할수있다. 또한그림 1의 State2 노드와같이최악실행시간과데드라인을가진태스크를명세할수있다. 트랜지션에는노드간의전이이벤트인가드와동기, 그리고상태전이시의데이터변수값할당등을기술할수있다. 동기에서이벤트를보낼경우에는! 기호를사용하며동기를받을때는? 기호를사용한다. 그림 1

3 안전성이중요한시간기반내장형소프트웨어의시간제약성검증에관한사례연구 649 그림 1 타임드오토마타의구성요소은 State1 노드에서 x > 3 조건을만족하면 event 동기를발생시키면서 x := 0 을할당하고최악실행시간 C와데드라인 D를가진태스크를수행하는 State2 노드로전이하는행위를보여준다. 명세된소프트웨어모델은 TIMES의시뮬레이션기능을통해서태스크스케줄링상태와명세모델의동작여부를확인할수있다. 시뮬레이션을통해서는부분적인실행시나리오에대한확인만가능한반면에검증기능을통해서는모델이가질수있는전체상태에대한확인이가능하고모델이주어진속성을만족하는지, 만족하지않는다면어떤경우에만족하지않는지를반례를통해서확인할수있다. 또한명세된모델은 TIMES에서제공하는코드생성기능을통해서코드로생성할수있다. 본연구에서는 TIMES의모델링, 시뮬레이션, 검증기능만을활용하였다. 2.2 유도조종장치본연구의대상시스템인유도조종장치의역할과특성은다음과같다. 유도조종장치는반응형시스템이다. - 유도조종장치는그림 2와같이비행시스템의제어에중추적인역할을하는장비로써비행시스템의현재상태를센서들로부터입력을받아서정보를처리하여주어진미션을수행할수있도록구동기들을제어하는반응형시스템이다. 유도조종장치는엄격한실시간제약성을갖는내장형시스템이다. - 유도조종장치는적시에유도및비행제어에필요한논리연산을수행하여유도조종명령생성과지상의발사통제장비및비행시스템내의각서브시스템들과의인터페이스를담당하는내장형시스템이다. 유도조종장치는안전성이중요한시스템이다. - 유도조종장치소프트웨어가유도조종장치의요구사항들을만족하지못하면자칫비행시스템의사고로이어져예기치않은인명피해와물리적손실을발생시킬수있다. 따라서높은안전성을갖는유도조종장치내장형소프트웨어의개발은비행시스템개발에서중요하다. 3. 유도조종장치소프트웨어분석및설계 3.1 요구사항분석그림 3은유도조종장치의유스케이스다이어그램을보여준다. 유도조종장치는발사전에는발사통제장비와의통신을통해비행시스템임무에필요한자료를수신하고각시스템들의준비상태확인등의발사절차임무를수행한다 [4]. 발사후에는유도조종명령을통해비행시스템내의각서브시스템들을제어하여비행임무를수행하며, 이때다른서브시스템들과의통신은주로 MIL-STD-1553B를통해이루어진다 [16]. 본연구는복잡한시간관련비기능요구사항을가지는비행임무수행유스케이스를대상으로소프트웨어의시간제약성을모델링하고검증하였다. 유도조종장치소프트웨어의비행임무에서시간과관련된주요비기능요구사항의예는표 1과같다. 비기능요구사항의내용으로는제어의존성, 시간제약성등의태스크행위명세에대한정보들이기술된다. NFR1은태스크들간의경쟁상태를최소화하기위해사용자수준에서태스크수행순서를미리결정하여적시에태스 그림 2 유도조종장치의역할도 그림 3 유도조종장치의유스케이스다이어그램

4 650 정보과학회논문지 : 소프트웨어및응용제 38 권제 12 호 ( ) 표 1 주요비기능요구사항예제 NFR1 태스크의실행순서는사용자수준에서제어한다. NFR2 NFR3 NFR4 NFR5 NFR6 시스템운영관련태스크에가장높은우선순위를부여한다. 이산입출력, 아날로그와디지털신호처리등의하드웨어제어작업을일정단위시간마다수행한다. 비행연산태스크 B 의수행에필요한입력데이터는태스크가수행되기전에비행시스템내의서브시스템들로부터수신되어야한다. 최초실행시비행연산태스크 A 의수행후에비행연산태스크 B 가수행되어야한다. 비행연산태스크 A - 수행주기 : 최악실행시간 : 데드라인이내 - 데드라인 : 20 비행연산태스크 B - 수행주기 : 최악실행시간 : 데드라인이내 - 데드라인 : 60 크들을수행하기위한요구사항이다. NFR2는태스크우선순위결정을위한요구사항으로시스템운영관련태스크를가장먼저처리해야함을의미한다. NFR3은하드웨어제어작업을일정시간마다수행하여비행시스템의최신상태를업데이트하고비행시스템을제어하기위한요구사항이다. NFR4와 NFR5는통신과태스크수행간의제어의존성에관한요구사항이다. NFR6 은태스크들의시간제약성조건으로수행주기와최악실행시간, 데드라인등으로구성된다. 3.2 개념설계개념설계단계에서태스크구성과태스크시간제약성정보가구체화된다. 본연구에서사용된소프트웨어모델은유도조종장치소프트웨어의통신과태스크들간의동기에초점을맞춘설계이며, 다음의 5개의태스크들로구성된다. SM (System Manager) SC (System Controller) CM (Communication Manager) A, B SM은시스템운영에관련된태스크로서매단위시간마다가장우선적으로처리해야하는작업을수행한다. SC는이산입출력, ADC(Analog-to-Digital Conversion), DAC(Digital-to-Analog Conversion) 등을통해유도조종장치하드웨어를제어한다. CM은 MIL-STD- 1553B 통신을송수신하여비행상태데이터를 B에게전달한다. A와 B는비행관련연산을처리하는태스크들이다. 태스크를효과적으로제어하기위해단위시간 20 마다 Tick이발생되며, 총 10개의 Tick 구간이반복된다. 예를들어, Tick 0 구간은시간 0에서 20 사이, 200 태스크 SM SC 표 2 태스크들의시간제약성예제 시작구간 매 Tick 구간 (Tick0~Tick9) Tick0, Tick2, Tick4, Tick5, Tick7, Tick9 최악실행시간 데드라인 우선순위 4 10 높음 5 20 중간 CM Tick0, Tick2, Tick4, Tick5, 5 20 중간 Tick7, Tick9 B Tick3, Tick 낮음 A Tick 낮음 에서 220 사이등을나타내고 Tick 9 구간은시간 180 에서 200 사이, 380에서 400 사이등을의미한다. 각태스크들의시간제약성정보는표 2와같다. 시작구간은각태스크들이실행되는시간이고, 데드라인은시작구간을기준으로한상대적인데드라인이다. 예를들어, 태스크 B가 Tick 3 구간인 260에서시작되면데드라인은 320이된다. 그림 4는 Tick 0 구간의시작이 200일경우에유도조종장치소프트웨어모델의태스크실행구조를보여준다. 태스크의최악실행시간을고려하지않은단지시작시점만을표시해서태스크들간의제어의존선과실행순서를보여주는그림이다. 그림 4에서흰색사각형은태스크를보여주고회색사각형은 MIL-STD-1553B 통신상태임을나타내며화살표는동기제어순서를보여준다. 먼저, 전체소프트웨어구조로높은안전성이요구되는항공이나의료분야의시스템소프트웨어에서많이사용하는시간기반구조가적용되었다 [17,18]. 시간기반구조는소프트웨어의행위를미리결정하여원하는시점에원하는작업을수행할수있어서 NFR1에서요구한사용자수준에서의태스크실행순서제어가가능하다. 매 Tick이발생되면 SM이먼저수행이되고 SC는비주기적으로수행되어비행시스템의현재상태를입력받아관련작업을수행하며그결과를비행시스템으로출력한다. CM은 MIL-STD-1553B 통신을관장하여데이터를송수신한다. Tick 2 구간과 Tick 7 구간에서 CM이수행되기위해서는태스크 B 수행에필요한데이터를수신했음을알리는 MIL-STD-1553B 통신종료동기와태스크 SC로부터의동기를모두수신해야한다. 이요건은 NFR1과 NFR4를충족해야함을의미한다. Tick 3 구간과 Tick 8 구간의태스크 B도 CM과 SM의동기를모두받아야실행가능하며, 이도마찬가지로 NFR1과 NFR4를준수해야함을의미한다. 태스크 A는 Tick 6 구간에서수행되며 SM의동기를받아야

반면에 SM과 SC 태스크는표 2의시작구간내에서태스크수행을완료해야한다. 4. 유도조종장치소프트웨어명세및검증 4.1 정형명세개념설계된유도조종장치소프트웨어모델을 TIMES 도구를이용해서타임드오토마타로정형명세하였다.

5 안전성이중요한시간기반내장형소프트웨어의시간제약성검증에관한사례연구 651 그림 4 소프트웨어모델의태스크실행구조 한다. 데드라인을고려한주요태스크들의실행구간을살펴보면태스크 A는 Tick 6 구간내에서만수행되어야하고, 태스크 B는 Tick 3 구간에서 Tick 5 구간까지와 Tick 8 구간에서 Tick 0 구간까지만수행되어야한다. 반면에 SM과 SC 태스크는표 2의시작구간내에서태스크수행을완료해야한다. 4. 유도조종장치소프트웨어명세및검증 4.1 정형명세개념설계된유도조종장치소프트웨어모델을 TIMES 도구를이용해서타임드오토마타로정형명세하였다. 그림 5는 TIMES 도구에서명세된유도조종장치소프트웨어의전체구성모델을보여준다. 명세모델에는 SM, SC, CM, A, B 모델외에실제통신을제어하는 MIL- STD-1553B 통신컨트롤러의행위를모델링한 CC (Communication Controller) 가환경모델로추가되었다. 그림 5 유도조종장치소프트웨어전체명세모델 그림 6은 SM의타임드오토마타모델로서총 21개의노드들과 21개의트랜지션들로구성된다. SM은 SM 고 그림 6 SM 의타임드오토마타모델

652 정보과학회논문지 : 소프트웨어및응용제 38 권제 12 호 (2011.12) 유의작업을수행하고다른모델에게보낼이벤트를결정하는 SM_Working 노드들과모델들에게이벤트를보낸후다음 Tick을기다리는Tick_Interval 노드들로구성되며, 노드의숫자는매 Tick의식별자를나타낸다. Tick은 SystemClock 변수를이용해서 20 단위로수행시간을제어한다.

예를들어, 그림 4의 Tick 6 구간을모델링하기위해 SM_Working6 노드에서 SystemClock >= 124 을만족할경우에태스크 A 수행을요청하는 AfaRun 이벤트를발생시킨다. 또한명세모델에서는 Tick 구간을상대시간으로모델링하였으며연속적인실행시간은 MissionTime 변수에저장된다. 그림 7은 CM을타임드오토마타로명세한모델을보여준다.

6 652 정보과학회논문지 : 소프트웨어및응용제 38 권제 12 호 ( ) 유의작업을수행하고다른모델에게보낼이벤트를결정하는 SM_Working 노드들과모델들에게이벤트를보낸후다음 Tick을기다리는Tick_Interval 노드들로구성되며, 노드의숫자는매 Tick의식별자를나타낸다. Tick은 SystemClock 변수를이용해서 20 단위로수행시간을제어한다. 예를들어, Tick1의구간은 SM_ Working1과 Tick1_Interval로구성되며 SystemClock 값은 20에서 40 사이가된다. 각 SM_Working 노드의시간조건에는표 2에명시된 SM의최악실행시간인 4 가할당되었고다음노드인 Tick_Interval로전이할경우에 SC, B, A에게해당이벤트동기를보내도록명세되었다. 예를들어, 그림 4의 Tick 6 구간을모델링하기위해 SM_Working6 노드에서 SystemClock >= 124 을만족할경우에태스크 A 수행을요청하는 AfaRun 이벤트를발생시킨다. 또한명세모델에서는 Tick 구간을상대시간으로모델링하였으며연속적인실행시간은 MissionTime 변수에저장된다. 그림 7은 CM을타임드오토마타로명세한모델을보여준다. 여기서 x, y는노드와트랜지션에서사용되는클락변수이다. CM 모델은총 6개의노드들과 11개의트랜지션들로구성되며다음과같이동작한다. 먼저, Ready 노드에서 SC로부터 DoComStart가수신되면클락변수 x를 0으로설정하고 TxRxStarting 노드로전이한다. TxRxStarting에서는 x 값이 5 이상일때에통신컨트롤러모델인 CC로 ComRequest 동기를보내고다음노드인 Waiting1로전이한다. CM이 DataCopying 노드로가는경우는먼저통신컨트롤러모델인 CC로부터통신종료동기인 ComIntr이수신되고나중에 SC로부터 DoComEnd이수신되는경우와그반대의경우가있다. Waiting11과 Waiting12 노드가이두가그림 7 CM의타임드오토마타모델 그림 8 B의타임드오토마타모델지경우를표현한다. Waiting1의 x <= 40 은통신요구후에두번째 Tick 구간에서동기를수신하기위한조건이고 Waiting11과 Waiting12의 y <= 10 은같은 Tick 구간에서두동기를처리하는행위를모델링한것이다. 통신컨트롤러로부터통신데이터를복사하는 DataCopying 노드의역할이종료되면 order 변수값에따라 DataReady를 B로송신하고 TxRxStarting 노드로가거나다시 Ready 노드로전이한다. 그림 8은비행관련연산을처리하는 B를명세한모델이다. B 모델은 5개의노드들과 7개의트랜지션들로구성된다. Waiting1과 Waiting2 노드를통해서 CM 모델의 DataReady 동기와 SM 모델의 BfaRun 동기를모두수신하면 Checking 노드에서태스크 A가먼저실행되었는지확인한다음에 RunB 노드에서태스크 B를수행한다. 4.2 정형검증도메인전문가가추출한유도조종장치소프트웨어모델이만족해야하는소프트웨어의속성을다음의 5가지범주로나누어 TIMES의모델체킹을통해자동적으로검증하였다. 정형검증결과는유도조종장치소프트웨어모델이모든범주의속성들을모두만족함을보였다. 데드락자유 (deadlock-freedom) - A[] (not deadlock) 데드락이발생하지않아야한다. 시스템클락 - A[] not (SystemClock > 200) 시스템클락이 200을넘지않아야한다. 도달성 (Rechability) - E<> (CM.Waiting11 or CM.Waiting12) 언젠가는 CM의 Waiting11 또는 Waiting 12 상태에도달하는경우가있어야한다.

안전성이중요한시간기반내장형소프트웨어의시간제약성검증에관한사례연구 653 - E<> (B.Waiting1 or B.Waiting.2) 언젠가는 B의 Waiting1 또는 Waiting2 상태에도달하는경우가있어야한다. 제어의존성 - A[] (Arun == 0 imply not B.RunB) 태스크 A가수행되지않으면태스크 B가수행되지않아야한다.

7 안전성이중요한시간기반내장형소프트웨어의시간제약성검증에관한사례연구 E<> (B.Waiting1 or B.Waiting.2) 언젠가는 B의 Waiting1 또는 Waiting2 상태에도달하는경우가있어야한다. 제어의존성 - A[] (Arun == 0 imply not B.RunB) 태스크 A가수행되지않으면태스크 B가수행되지않아야한다. 태스크데드라인 - A[] (SCHEDULER.RUN_SCtask imply SM.Tick0_Interval or SM.Tick2_Interval or SM.Tick4_Interval or SM.Tick5_Interval or SM.Tick7_Interval or SM.Tick9_Interval) SC는 Tick 0, 2, 4, 5, 7 또는 9 구간에서만수행되어야한다. - A[] (SCHEDULER.RUN_Atask imply SM.Tick6_Interval) A는 Tick 6 구간에서만수행되어야한다. - A[] (SCHEDULER.RUN_Btask imply SM.Tick3_Interval or SM.SM_Working4 or SM.Tick4_Interval or SM.SM_Working5 or SM.Tick5_Interval or SM.Tick8_Interval or SM.SM_Working9 or SM.Tick9_Interval or SM.SM_Working0 or SM.Tick0_Interval) B는 Tick 3, 4, 5, 8, 9 또는 0 구간에서만수행되어야한다. 4.3 반례생성과활용정형검증시에명세모델이만족하지않는속성을사용하면모델체커는그이유를설명하는반례를생성하며반례는명세모델의검증과이해에유용하게사용된다. 본연구의초기명세모델도반례생성을통해명세모델의오류와모델속성의오류를분석할수있었다. Tick3 에서태스크 B 가수행되지않음 태스크 A 종료 Tick6 에서태스크 B 수행 Tick8 에서태스크 B 가수행되지않음 이전태스크 B 가종료되지않은상태에서 Tick 9 에서태스크 B 수행요구됨 스케줄링에러발생 데드락발생 그림 10 명세오류를갖는 B 모델의검증반례 시간명세가없는 Checking 노드 그림 9 B 의초기타임드오토마타모델 그림 9는 B의초기타임드오토마타모델로서그림 8 과의차이점은 Checking 노드에시간명세가되지않은것이다. Checking 노드는태스크 A가먼저실행되었는지판단하는역할을하며실행에많은시간이필요하지않고 RunB 노드로즉시전이해야하는노드이다. 하지만 Checking 노드에시간명세가되지않은그림 9

8 654 정보과학회논문지 : 소프트웨어및응용제 38 권제 12 호 ( ) 다. 따라서검증에사용한모델속성의오류로판정하여태스크 B의검증속성을수정하였다. 5. 평가 Tick8에서태스크 B 수행 Tick9에서태스크 B 수행 Tick0에서태스크 B 수행그림 11 속성오류를가지는 B 모델의검증반례의 B 모델은데드락자유검증에서그림 10과같은반례를생성하였다. 반례는명세된오토마타모델들과태스크를처리하는가상스케줄러간의상태와이벤트들로구성된다. 그림 10에대한반례분석을통해태스크 B 가그림 4의설계된태스크실행구조를만족하지않음을확인하였다. 태스크 B가설계된 Tick 3 구간에서수행되지못하고지연되어 Tick 6 구간에서수행되었고다음태스크 B도 Tick 8 구간이아닌 Tick 9 구간에서수행되었다. 또한이전태스크 B가종료되지않은상태에서다음태스크 B가수행되어스케줄링에러가발생되었고전체모델의실행구조에영향을주어 Tick9_ Interval에서데드락이발생하였다. 따라서그림 8과같이 Checking 노드에대한시간명세를통해태스크의시작구간을제어해야함을알수있었다. 정형검증초기에태스크 B의데드라인검증속성으로아래와같은속성을사용하였으며, 검증에서그림 11 과같은반례를얻었다. - A[] (SCHEDULER.RUN_Btask imply SM.Tick3_Interval or SM.SM_Working4 or SM.Tick4_Interval or SM.SM_Working5 or SM.Tick5_Interval or SM.Tick8_Interval or SM.SM_Working9 or SM.Tick9_Interval) 그림 11의반례분석을통해태스크 B는 Tick 3 구간에서 Tick 5 구간까지와 Tick 8구간에서그다음 Tick 0 구간까지수행하도록설계되었으므로 Tick 0 구간에서태스크 B의수행이정상적인동작임을확인하였고검증속성에서 Tick 0 구간인 SM.SM_Working0 과 SM.Tick0_Interval이포함되지않은것을확인하였 유도조종장치소프트웨어모델링에서태스크의행위명세수준을결정하는데어려움이있었다. 하지만, 본연구의목적에부합하도록각태스크의상세기능명세보다는수행시간명세수준에서모델링이진행되었다. 초기명세모델의시간제약성검증에는많은데드락이발생하였다. 반례를통한데드락의원인분석결과는 4.3절에서서술한바와같이초기오토마타모델의노드와트랜지션에클락변수의조건이구체적으로모델링되지않아서한노드의수행이끝난시점에서다음전이가가능한노드가없어데드락이발생함을보여주었다. 시간제약성검증을위한올바른오토마타모델을작성하기위해서는시간과관련된요구사항들의분석을통해타임드오토마타모델에시간제어정보를정확히명세해야함을확인했다. 본사례연구에사용된대상시스템의요구사항은이미잘정의된내용으로모델링과정에서요구사항과관련된시간에러가발견되지않았으나모델명세및검증과정에서태스크행위명세에대한검토가다시면밀히이루어지는효과를얻었다. 이를통해서요구사항단계에서의잠재된에러들을효과적으로찾아낼수있고태스크행위명세를더욱구체화할수있으므로강건한소프트웨어모델을생성할수있을것이다. 도메인경험에의하면유도조종장치는비행시스템개발이진행되면서다양한임무와서브시스템들이추가되므로유도조종장치내장형소프트웨어가진화할수록시간제약성문제에더욱민감해진다. 따라서초기설계단계에서다양한시간제약성과태스크수행시나리오를가진유도조종장치타임드오토마타모델들을명세하여검증함으로써적절한태스크행위명세와실행구조를결정하는데본연구를활용할수있다. 모델체킹기법을성공적으로사용하기위해서는충분한소프트웨어행위에대한이해와이를기반으로한모델링과검증하고자하는소프트웨어속성추출이중요하며시간정보에대한충분한자료가필요하다. 탐색개발과체계개발로구성되는유도조종장치개발에서는탐색개발단계에서얻어지는유도조종장치프로토타입이나평가장비를통해서시간정보를얻을수있으므로모델체킹기법을효과적으로적용할수있으리라판단된다. 또한본연구에서수행한모델명세와검증방법은비단유도조종장치와같은시간기반내장형소프트웨어뿐만아니라이벤트기반구조를가진내장형소프트

9 안전성이중요한시간기반내장형소프트웨어의시간제약성검증에관한사례연구 655 웨어에도적용할수있으며 TIMES가아닌다른실시간모델체킹도구들도실시간내장형소프트웨어의시간제약성검증에사용할수있다. 이를통해서시간제약성만족이중요한내장형소프트웨어의설계단계에서시간제약성속성들을검증함으로써소프트웨어개발비용을줄일수있을것이다. 6. 관련연구 6.1 실시간시스템의행위검증을위한실시간모델체커실시간시스템의행위검증을위해사용되는모델체킹도구로써 TIMES 외에 UPPAAL[10], PAT[11], TSMV[12], KRONOS[13] 등이있다. UPPAAL[10] 은실시간시스템의행위를타임드오토마타의네트워크로써명세하는모델체킹도구이다. TIMES와같이시뮬레이션을통해명세된시스템의동작을확인할수있고 CTL로작성된속성으로명세모델을검증할수있다. PAT[11] 는 IRL(Intermediate Representation Layer) 이라는계층구조를채택하여모델링언어와모델체킹알고리즘을분리함으로써다양한언어와검증논리를사용할수있다. 따라서실시간시스템뿐만아니라웹서비스, 센서네트워크등다양한분야에적용할수있는장점을가진다. TSMV[12] 는타임드 Kripke 구조상에서명세된시스템의행위를 TCTL로검증하는심볼릭모델체커로써 NuSMV을이용해서구현되었다. PCI 로컬버스와교량횡단문제에적용된사례연구가있다. KRONOS[13] 는타임드오토마타로시스템을명세하고 TCTL로검증하는모델체커로써 TIMES나 UPPAAL 과는달리그래픽이나시뮬레이션기능을지원하지않으며, 모델을텍스트로명세하여검증한다. 6.2 실시간내장형시스템의시간제약성검증에모델체커를활용한연구 Barreto[19] 는 C 언어를사용하는내장형시스템의구현단계에서원본코드에시간분석도구나도메인전문가로부터얻은시간제약성정보를첨부하고 ESBMC 모델체커를이용하여시간제약성을검증하는방법을제안한다. 사례연구로의료분야에서사용되는펄스옥시미터 (pulse oximeter) 의구현코드에대한시간제약성검증을수행하였다. 본논문이설계단계에서실시간모델체커를이용한것에반해 Barreto 연구는비시간모델체커를이용해서구현코드수준에서시간제약성을검증하였다. Mikučionis[20] 는 UPPAAL를이용한스케줄링가능성분석을위한모델링프레임워크를제안하였다. 본연 구와같이실시간모델체커를이용하여실시간시스템의시간제약성을검증한점에서유사하다. Mikučionis 는스케줄링가능성문제를타임드오토마타의도달성문제로변환하고이를실시간모델체커로검증하기위해서고정우선순위방식의선점형스케줄러와유휴태스크를위한모델을제안하였고인공위성시스템을대상으로사례연구를하였다. 7. 결론과향후연구 본논문은국방분야의실시간내장형소프트웨어인유도조종장치소프트웨어설계에모델체킹기법을국내에서처음적용한사례연구의결과이다. 본논문에서는유도조종장치소프트웨어를정형기법을지원하는자동화도구인 TIMES를이용하여태스크를가지는확장된타임드오토마타모델로명세하고시간제약속성들을검증하였으며, 반례를통해명세모델과속성의오류를찾아낸과정을보였다. 검증결과로부터유도조종장치소프트웨어모델이시간제약속성들을만족함을확인하였으며, 모델수준에서유도조종장치소프트웨어의시간제약성검증방법의적용가능성을확인하였다. 향후연구로다양한시간제약성검증이가능하도록유도조종장치소프트웨어모델의확장을계획하고있으며, 검증된명세모델로부터시간제약성을만족하는코드를자동생성하는연구를계획하고있다. 참고문헌 [1] J. Xu, D. L. Parnas, "On Satisfying Timing Constraints in Hard-Real-Time Systems," IEEE Transactions on Software Engineering, vol.19, no.1, Jan [2] J. Choi, J. Shim, S. Yim, "The Implementation and Performance Analysis of Soft Timer Interrupt UML-RT Model on a Windows Platform with Real-Time Extension," Proc. of the Korea Information Science Society Fall Conference, vol.32, no.2, pp , (in Korean) [3] Hassan Gomaa, Designing Concurrent, Distributed, and Real-Time Application with UML, Addison- Wesley, [4] D. Sang, G. Kim, J. Choi, "A Result Report of SSM HILS," Agency for Defense Development, Feb (in Korean) [5] Constance Heitmeyer, Dino Mandrioli, Formal Methods for Real-Time Computing, John Wiley & Sons, [6] E. M. Clarke, Jr., O. Grumberg, D. A. Peled, Model Checking, The MIT Press, [7] T. Amnell, E. Fersman, L. Mokrushin, P. Pettersson, W. Yi, "TIMES: a Tool for Schedulability Analysis and Code Generation of Real-

656 정보과학회논문지 : 소프트웨어및응용제 38 권제 12 호 (2011.12) Time Systems," In Proc. of FORMATS 03, Lectures Notes in Computer Science, Springer-Verlag, 2003.

Fersman, P. P. Pettersson, H. Sun, and W. Yi, "Code Synthesis for Timed Automata," Nordic Journal of Computing, vol.9, no.4, pp.269-300, 2002. [10] G.

[11] Yang Liu, Jun Sun and Jin Song Dong, "PAT 3: An Extensible Architecture for Building Multidomain Model Checkers," The 22nd annual International Symposium on Software Reliability Engineering

10 656 정보과학회논문지 : 소프트웨어및응용제 38 권제 12 호 ( ) Time Systems," In Proc. of FORMATS 03, Lectures Notes in Computer Science, Springer-Verlag, [ 8 ] Uppsala University Design and Analysis of Real- Time Systems team, "TIMES-a tool for modeling and implementation of embedded systems," 2007, [9] T. Amnell, E. Fersman, P. P. Pettersson, H. Sun, and W. Yi, "Code Synthesis for Timed Automata," Nordic Journal of Computing, vol.9, no.4, pp , [10] G. Behrmann, A. David, and K. G. Larsen, A Tutorial on Uppaal, Department of Computer Science, Aalborg University, Denmark, Nov [11] Yang Liu, Jun Sun and Jin Song Dong, "PAT 3: An Extensible Architecture for Building Multidomain Model Checkers," The 22nd annual International Symposium on Software Reliability Engineering (ISSRE 2011), Hiroshima, Japan, Nov Dec. 2, (Accepted) [12] N. Markey and Ph. Schnoebelen, "Symbolic model checking of simply-timed system," In Y. Lakhnech and S. Yovine, editors, Proceedings of the Joint Conferences Formal Modelling and Analysis of Timed Systems (FORMATS 04) and Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 04), volume 3253 of Lecture Notes in Computer Science, pp Springer, [13] Sergio Yovine, "Kronos: a verification tool for real-time systems," Journal on Software Tools for Technology Transfer, Oct [14] A. David, J. Illum, K. G. Larsen, A. Skou, Model- Based Framework for Schedulability Analysis Using UPPAAL 4.1. In Model-Based Design for Embedded Systems, pp CRC Press, Boca Raton [15] E. Fersman, P. Pettersson, W. Yi, "Timed Automata with Asynchronous Processes: Schedulability and Decidability," Proc. of TACAS 02, pp.67-82, [16] J. Choi, Y. Kwon, "MIL-STD-1553B IRS for SSM," Agency for Defense Development, Sep (in Korean) [17] Michael J. Pont, "Reducing the time taken to test your next embedded system," TTE Systems Ltd., [18] Michael J. Pont, Patterns for Time-Triggered Embedded Systems, Addison-Wesley, [19] R. S. Barreto, L. Cordeiro, B. Fischer, "Verifying Embedded C Software with Timing Constraints using an Untimed Model Checker," CoRR abs/ , [20] M. Mikučionis, K. G. Larsen, J. I. Rasmussen, B. Nielsen, A. Skou, S. U. Palm, J. S. Pedersen, and P. Hougaard, "Schedulability Analysis Using Uppaal: Herschel-Planck Case Study," ISoLA (2): pp , 최진호 1997년홍익대학교컴퓨터공학과졸업 ( 학사 ). 1999년홍익대학교컴퓨터공학과졸업 ( 석사 ). 1999년~2001년육군전산소소프트웨어개발병. 2002년~현재국방과학연구소연구원. 2009년~현재한국과학기술원전산학과박사과정. 관심분야는소프트웨어공학, 모델기반내장형소프트웨어설계, 실시간내장형시스템, 소프트웨어안전성, 정형검증 지은경 1999 년 KAIST 전산학과학사 년 KAIST 전산학과석사 년 ~2002 년몽골울란바타르대학전임강사 년 ~2004 년 ( 주 ) 이마린로직스소프트웨어엔지니어 년 KAIST 전산학과박사 년 ~2011 년 University of Pennsylvania 박사후연구원 년 ~ 현재 KAIST 전산학과연구조교수. 관심분야는소프트웨어공학, 소프트웨어테스팅, 정형검증, 안전필수소프트웨어, 소프트웨어안전성 김현정 2005년서강대학교컴퓨터공학과졸업 ( 학사 ). 2007년한국과학기술원전산학과졸업 ( 석사 ). 2009년~2010년 University of Texas at Dallas 방문연구과정 년~현재한국과학기술원전산학과박사과정. 관심분야는모델기반테스팅, 소프트웨어안전성분석, 결함트리분석 배두환정보과학회논문지 : 소프트웨어및응용제 38 권제 6 호참조

DBPIA-NURIMEDIA

DBPIA-NURIMEDIA 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