한국시뮬레이션학회논문지 Vol. 21, No. 3, pp. 1-9 (2012. 9) http://dx.doi.org/10.9709/jkss.2012.21.3.001 DEVS 형식론을이용한공항 PAR 관제시스템자동화방안검증 성창호 1 구정 2 김탁곤 1 김기형 3 Verification of Automatic PAR Control System using DEVS Formalism Changho Sung Jung Koo Tag Gon Kim Ki-Hyung Kim ABSTRACT This paper proposes automatic precision approach radar (PAR) control system using digital signal to increase the safety of aircraft, and discrete event systems specification (DEVS) methodology is utilized to verify the proposed system. Traditionally, a landing aircraft is controlled by the human voice of a final approach controller. However, the voice information can be missed during transmission, and pilots may also act improperly because of incorrectness of auditory signals. The proposed system enables the stable operation of the aircraft, regardless of the pilot s capability. Communicating DEVS (C-DEVS) is used to analyze and verify the behavior of the proposed system. A composed C-DEVS atomic model has overall composed discrete state sets of models, and the state sequence acquired through full state search is utilized to verify the safeness and the liveness of a system behavior. The C-DEVS model of the proposed system shows the same behavior with the traditional PAR control system. Key words : DEVS (Discrete Event Systems Specification), PAR (Precision Approach Radar), Verification 요 본논문에서는공항정밀접근항공기의안전성을증대시키기위한방법으로 S/W 패킷모뎀을이용한 PAR 관제자동화방안을제안하고, DEVS 형식론을이용하여제안하는시스템의기능을검증하였다. 기존의 PAR 관제는음성으로항공기를통제함으로써조종사의정보획득능력이떨어질수있다. 이를해결하기위하여디지털신호에의한자동관제시스템을제안하고, 공항의 PAR이추적하고있는항공기의비행경로, 강하각, 거리를조종사에게실시간으로전송해주고일반화함으로서관제사의숙련도와관제특성에기인하는요소를배제할수있다. 제안된시스템의동작을검증하기위하여확장된 DEVS 형식론인 C-DEVS 형식론을사용하고, 하나의모델로합성된원자모델을통해시스템의전체상태시퀀스를검색하여시스템의안전성 (Safeness) 과필연성 (Liveness) 을검증할수있다. 제안하는시스템의 C-DEVS 모델을기존의음성관제시스템과비교하여두시스템이동일한상태시퀀스를가짐을확인하였으며, 모든상태를검증함으로써실제상황에적용할수있을것으로생각된다. 주요어 : 이산사건시스템형식론, 공항정밀접근레이더, 시스템검증 약 1. 서론 * 이논문은 2011년한국과학기술원 BK21 전자통신기술사업단에의하여지원되었습니다. 접수일 (2012년 6월 27일 ), 심사일 (1차 : 2012년 8월 24일 ), 게재확정일 (2012년 9월 11일 ) 1) KAIST 전기및전자공학과 2) 공군작전정보통신단 3) 아주대학교정보컴퓨터공학부주저자 : 성창호교신저자 : 성창호 E-mail; chsung@smslab.kaist.ac.kr 현재많은국제공항및공군비행기지의대부분은 PAR(Precision Approach Radar) [1] 정밀접근체계를보유하고있으며 [2,3], PAR의최종접근관제는음성에의해이루어진다. 음성에의한최종접근관제는비행정보제공의양이부족하고정확도가떨어지며, 신속성및적시성에있어일정한시간지연이발생함으로서관제효율성이저하될수있다. 이로인한항공기사고위험성을예방하 제 21 권제 3 호 2012 년 9 월 1
성창호 구정 김탁곤 김기형 기위해, 본논문은기존의음성관제시스템을보완하여디지털정보에의한자동화된시각관제시스템을제안하고그동작의정확성을검증한다. 자동화된 PAR 관제시스템은관제에필요한정보를모두디지털신호로변환하여조종사에게주기적으로제공한다. 제공하는정보는항공기에장착되어있는 UMPC 모니터에표시되며조종사는시각정보를이용하여항공기를제어한다. 제안하는 PAR 관제시스템은음성으로이루어지는기존의관제와비교하여동일한관제순서를가질것으로판단되며, 관제효율성또한증가할것이라판단된다 [4,5]. 각시스템의동작을모델링하기위하여이산사건시스템명세 (Discrete Event Systems Specifications, DEVS) [6] 를이용한다. 두시스템이동일하게동작함을검증하기위하여, 우선각시스템의안전성 (Safeness) 과필연성 (Liveness) 을검증하여각시스템의설계오류여부를확인하고, 그후두시스템내부에서발생하는모든상태시퀀스가일치하는지를확인한다. 시스템검증을위해확장된 DEVS 형식론인 C-DEVS(Communicating DEVS) 형식론을이용한다. C-DEVS 형식론은모델들사이의프로토콜을하나의수학적인모델로표현함으로써시뮬레이션없이시스템의기능검증을가능하게한다. 본논문구성은다음과같다. 우선 2장에서기존 PAR 관제시스템및검증과관련된연구에대해논의해본다. 3장에서는시스템동작검증에사용되는 C-DEVS 형식론에대해서살펴보고, 4장에서제안하는 PAR 자동관제시스템과그모델들에대해설명한다. 5장에서는제안하는시스템을검증하고, 6장에서결론을맺는다. 2. 관련연구 항공기의안전한착륙을위하여정밀접근시스템에대한연구가끊임없이진행되었으며, 현재 PAR, TLS (Transponder Landing System), ILS(Instrument Landing System), MLS(Microwave Landing System) 등, 수많은체계가개발되어운용되고있다. 정밀접근 (Precision Approach) 이라함은 국제민간항공기구 (ICAO) 부속서 (Annex) 10 ( 항공통신 ) 의정밀기준에부합하는진로와항공로이탈정보를제공하는항행안전무선시설을이용하는계기접근절차 로규정하고있다 [1]. PAR은비행기지에배치된레이더를이용하여항공기의경로를제공하는장비로전천후사용이가능한항공기접근및착륙유도장 비이다. 이는레이더포착항적자료를기준으로기존의음성통신장비를이용하여항공기의접근을유도함으로서 ILS와유사한공항접근방법구현을통해효율성을증대시킬수있다. 즉 PAR은항공기의경로 (Azimuth) 와강하각 (Glide Slope) 정보를음성을이용하여제공함으로써 ILS 계기를장착하고있지못한항공기에도사용할수있으며, 공항접근 Category I을만족할수있는능력을지니고있다. 그러나이와같은음성정보를이용한관제는다음과같은단점을가지고있다. 음성정보와시각정보의차이를다룬인간공학적연구결과를보면, 네트워크중심작전사례연구에서 Link-16 유 / 무에따른공대공전투에서청각기관의사용에서조종사들은전송된정보중약 70% 가량만을청취하며, 나머지는잘못전달되는것으로보고되고있다 [7]. 디지털데이터전송을통한시각적시현은수신된데이터를지속적으로시현함으로써잘못된인지가능성을대폭줄일수있다. 그리고동일정보를중복적으로부호화하는것은처리속도를높여주며 [8], 시각기관과청각기관으로부터의정보입력이상호갈등적으로주어질때나시각과청각과제가동시에수행될때에는시각우세 (Visual dominance) 현상이발생한다 [9]. 그러므로비행에있어조종사의시각기관은착시의가능성을내포하고있다할지라도시각기관이확실한감각기관인것은분명하며, 항공기를조종함에있어시각참조에의한조종이청각적인지를바탕으로조종을수행하는것에비해더우수하다는것을짐작할수있다. 이와같은관련연구를바탕으로항공기의공항접근경로와강하각정보를디지털로제공하여조종사에게시각적으로시현하여관제하는시스템을제안하고, 제안하는시스템의설계및기존시스템과의동작일치성을검증한다. 3. C-DEVS 를이용한시스템설계검증 제안하는시스템의설계를검증하는것은동작의정확성을검증하는것으로, 기존시스템의동작순서와동일하게작동하는지를확인하는것이다. 시스템동작검증을위해확장된 DEVS 형식론인 C-DEVS 형식론을사용하였다 [10]. C-DEVS 는이산사건시스템의동작을분석하기위해고안된방법론으로서, 두개이상의모델이서로결합되어있을때전체모델의동작을검증하기위해사용된다. 두모델을각각 AM i 과 AM j 라고할때, 두모델은다음과같은하나의합성원 2 한국시뮬레이션학회논문지
DEVS 형식론을이용한공항 PAR 관제시스템자동화방안검증 자모델로표현된다 [11]. AM i AM j = <E, S, T, ta, {AM i, AM j}> E: 이벤트집합 S: 합성원자모델의상태집합 T: 합성원자모델의상태천이관계 ta: 시간전진함수 E = (X i Y i { }) (X j Y j { }), X i, Y i: AM i 의입출력이벤트, X j, Y j: AM j 의입출력이벤트 S S i S j T S E S ta: S R + 0, 이때, C-DEVS 모델의각상태별시간은두모델의상태시간의최소값을취한다. C-DEVS 형식론에의해합성된하나의원자모델로상태천이및이벤트순서를확인함으로써모델의전체동작을검증한다. 그림 1과같이 SENDER 와 RECEIVER 로이루어진핑퐁프로토콜을표현하는두개의 DEVS 모델이있다. SENDER 는 send 상태에서머무를수있는시간 ST(!m) 이후에메시지를생성해서보내고, receive 상태에서 ack 메시지가오기를기다린다. 이때 timeout 시간이전에 ack 메시지가오거나메시지없이 timeout 시간이지나면 send 상태로바뀐다. 한편, RECEIVER 는 receive 상태에서 msg 메시지를받으면 accept 상태로천이하고, 일정시간 ST(!a) 이후에 ack 메시지를전송하고 receive 상태 로돌아간다. 이핑퐁프로토콜에서두모델간전송되는메시지중 msg 는제대로전송된다고가정하고, ack는손실이발생할수도있다고가정한다. 시뮬레이션없이두모델의기능을검증및분석하기위해두모델을합성하여하나의 C-DEVS 모델로표현한다. C-DEVS 모델을이용하여모델간프로토콜의안전성 (Safeness) [12] 과필연성 (Liveness) [13] 을검증하고, 두모델의상태시퀀스가동일함을검증할수있다. 안전성은모델내의통신프로토콜이데드락 (Deadlock) 이없음을의미하고, 필연성은프로토콜이라이브락 (Livelock) 없이언젠가는목적을달성하여시뮬레이션을종료함을의미한다. 제안하는시스템의기능검증은기존프로토콜의상태시퀀스와의동일성을확인하는것이다. 핑퐁프로토콜의 C-DEVS 모델은그림 2와같이하나의합성된원자모델로표현되며, 모델의상태시퀀스는다음과같다. ((SD,RV), ST(!m)) ((RV,AP), ST(!a)) ((SD,RV), ST(!m)) ((SD,RV), ST(!m)) ((RV,AP), ST(!a)) ((RV,RV), timeout-st(!a)) ((SD,RV), ST(!m)) 첫번째경우는메시지전달이성공한경우이고, 두번째경우는메시지전달이실패한경우이다. 핑퐁프로토콜은메시지전달의성공또는실패의반복으로이루어지며, 두개의상태천이로모델의동작을모두표현할수있다. 통신프로토콜의안전성과필연성을검증하기위한상태시퀀스를살펴보면, 하나의상태에머무르지않고성공또는실패시퀀스가반복됨을알수있다. 그러므로이통신프로토콜은데드락이없으므로안전성을만족한다고할수있다. 만약프로토콜이 10개의메시지를전송하는것이목적이라면, 언젠가는그목표를달성하게되 그림 1. 핑퐁프로토콜의 DEVS 모델 그림 2. 핑퐁프로토콜의 C-DEVS 모델 제 21 권제 3 호 2012 년 9 월 3
성창호 구정 김탁곤 김기형 관제가관제사의음성으로이루어졌다면, 제안하는관제시스템은디지털전송방법에의한자동화시스템이다. 관제상황및시나리오는다음과같다. 그림 3. DEVS 모델검증 / 분석및시뮬레이션방법론 므로, 필연성을만족한다고할수있다. 그림 3은 DEVS 모델을사용하여시스템의동작을이해하는개념을나타내고있다. DEVS 모델의기능을검증하고분석하기위해서여러원자모델을하나의합성된 C-DEVS 원자모델로나타낼수있고, 시뮬레이션엔진을이용하여 DEVS 모델을실행하여동작을확인할수있다. 이두방법의가장큰차이점은상태의전체검색 (Full search) 가능여부이다. C-DEVS 모델은각모델들의가능한모든상태들의집합으로이루어진상태의천이로이루어져있기때문에상태를전체검색하여모든상태시퀀스를찾아서확인할수있다. 그러나시뮬레이션을이용한검증은정해진시나리오에의해실행된결과만을확인하기때문에검색되지않는상태들도존재하게된다. 예를들어통신두절로인한상태변화는실제환경이아니면시뮬레이션을통해확인하기어려운경우이다. 물론가능한모든시나리오를이용하여시뮬레이션하면검증이가능할수도있으나, 시나리오선정및실행에따르는시간과비용이많이든다는문제점이있다. 그러므로시스템의기능검증및분석을위하여하나의합성된 C-DEVS 모델을이용하는것이가장효과적이며, 제안하는 PAR 자동관제시스템을검증하기위해 C-DEVS 형식론을사용하고자한다. 4. PAR 자동관제시스템 PAR 자동관제시스템을모델링하기위해서는기존의음성을이용한관제와제안하는디지털정보를이용한관제의절차를살펴보는것이필요하다. 4.1 시스템요구사항관제시스템은관제사와조종사로이루어지며, 기존의 4.1.1 관제상황설명 [14][15] 비행기지로 PAR 접근을수행할경우최초에는 Radar Approach Control 에서관제를유도하여 Final 진입시약 10NM 이전에 Final Approach Controller 에게인계한다. 최종적으로고도는실고도 2000ft 를유지시키며, 약 7 ~ 8NM 정도에서 Begin Descent 를지시하고, 조종사는 3도의 Glide Slope으로강하를시작하여결심고도 (Decision Height, DH) 까지 2~3분정도의강하비행을한다. Final 관제사는접근항공기를관제함에있어 5초이내의끊김없는음성정보를제공하여항공기를관제한다. 관제는음성에의한관제, 혹은데이터전송에의한관제를수행하고, 조종사는음성에의한관제와데이터전송에의한관제에서동일하게반응하는것으로간주한다. 4.1.2 기존의음성에의한관제 [16] PAR Final 관제사는접근항공기를관제함에있어 5 초이내의끊김없는관제정보를제공하고있다. 그러나관제사의음성에의한관제는항공기의거리, 경로, 강하각정보를신속하게제공할수없는한계를가진다. 관제사는경로와강하각중오차범위나변화율이큰것부터관제정보를제공할것이다. 관제에서는주어진상황에적합한가장필요한정보 1가지만을음성으로제공할수있다. 관제에필요한용어를선택하는판단시간은 1초로하였다. 본정보를제공하기위해서는평균 5초의시간이소요되는것으로간주하고, 다음정보를제공하기위해서는짧은호흡에필요한 2초의여유시간을가지며, 2회의정보를제공한후 4초의호흡시간을가지는것으로가정한다. 4.1.3 제안하는디지털정보에의한관제관제자료를디지털데이터형식으로제공하는것은매우간단하다. 관제에필요한자료를지속적으로전송할수도있으나이렇게할경우 Radio에무리를주게된다. 그러므로관제자료를지속적으로전송하지않도록하기위해서변화율을계산하여경로와강하각및이의변화율을동시에전송하는것이필요하다. 변화율은항공기의관성을고려하여 PAR에서제공해주어야할최대시간을결정하였으며, 본논문에서는이양자를고려하여전송주기를 2.5초로설정하였다. 경로는경로수정에필요한항 4 한국시뮬레이션학회논문지
DEVS 형식론을이용한공항 PAR 관제시스템자동화방안검증 그림 4. PAR 정밀접근자동화체계구성개념 공기의비행방향정보를동시에제공해주며, 총 18 byte의정보를매 2.5초마다 1회전송하여조종사에게알려준다. 그림 4는제안하는디지털정보에의한 PAR 정밀접근자동화체계의구성개념을보여주고있다. PAR의항적정보를 PC로연동하고, 이를적절한형태로가공하여 S/W 패킷모뎀과 U/VHF Radio를통해항공기에전송한다. 항공기에서는 S/W 패킷모뎀을통해수신된정보를 UMPC 에전시함으로써경로와강하각, 거리에대하여 ILS 계기와같은형태로표현하여조종사에게제공해준다. 그림 5. 음성에의한 PAR 관제시스템 DEVS 모델 4.1.4 조종사의항공기조종을위한반응음성에의한관제이든, 디지털정보제공에의한관제이든정보를접할경우조종사는다음과같은반응을보이는것으로간주한다. 계기지시나음성을통해조종사가인지하는시간은일반적인남자의경우반응시간이 0.1 0.3초임을감안하여 0.2 초로설정하였다. 조종사가상황을판단하여조종간의움직임을통해자세계상에서자세를맞추는조작을수행하는시간은 1초로설정하였고, 조종간의움직임을통해항공기가반응하는데필요한지연시간도 1초를적용하여총 2.2초의자세수정에필요한시간을설정하였다. 4.2 각시스템의 DEVS 모델링음성및디지털관제시스템과조종사를 DEVS 모델로표현하면다음과같다. 우선음성에의한관제시스템모델은그림 5와같다. 초기의 Decide 상태에서 5초동안정보를보내고 (1 st Info), 짧은호흡후 (Short Breath) 결심고도에도달했다는이벤트가발생할시관제를종료하고 (Finish), 그렇지않으면다음정보를전송한다 (2 nd Info). 그리고긴호흡후 (Long Breath) 다음정보를준비한다. 5초이상의통신두절로인해조종사가관제를받지못할시실패이벤트를받게되고관제는종료하게된다 (Fail). 그림 6. 디지털정보에의한 PAR 관제시스템 DEVS 모델디지털정보에의한 PAR 관제시스템 DEVS 모델은그림 6과같이간단하게표현된다. 매 2.5초마다정보를보내고 (Send), 결심고도도달 (Finish) 또는관제실패시 (Fail) 발생하는이벤트에의해관제가종료된다. 조종사는음성에의한관제와디지털정보에의한관제모두동일하게반응한다. 조종사의 DEVS 모델은그림 7 과같이표현된다. 프로토콜의제약사항인 5초이내의끊김없는관제신호를고려해야하므로, 초기상태에서 5초동안머무르면서 (Init) 어떠한관제신호도들어오지않는다면통신두절 (Lost communication) 로판단한다 (Fail). 만약음성신호가들어온다면음성관제가끝날때까지기다리고 (Receive) 음성이끝난후항공기를조종하고 (Operation) 다음신호를기다린다 (Wait). 디지털신호의 제 21 권제 3 호 2012 년 9 월 5
성창호 구정 김탁곤 김기형 그림 7. 조종사를묘사하는 DEVS 모델 경우모니터상에정보가바로나타나므로시각적으로인지한후바로항공기를조종한다. 조종후결심고도에도달시 PAR 관제를종료하고최종적으로착륙한다 (Finish). 조종시간을포함하여 5초동안관제신호가들어오지않으면통신두절로판단하고 PAR 관제실패로관주한다. 5. 검증및평가 제안된디지털전송에의한관제시스템의기능을검증하기위하여 C-DEVS 형식론을사용하고, 전체상태검색을통해가능한모든상태시퀀스를추출하여두시스템을비교한다. 5.1 기존의음성에의한관제음성에의한관제시스템과조종사사이의프로토콜을하나의모델로합성하면그림 8과같다. 음성정보는통신상태에따라조종사에게전송되지않을수있음을가정하며, 이로인한통신두절을합성된모델에표현한다. 이이벤트는 (!command_start, ) 형태로표현되며, 송신모델에서는메시지를보냈으나수신모델에서받지못하는것을의미한다. 그림 8의합성된모델에서모든상태시퀀스를추출하면다음과같다. 1) (Decide, Init, [1s]) (1 st Info, Receive, [5s]) (Short Breath, Operation, [1.2s]) (Short Breath, Wait, [0.8s]) (2 nd Info, Receive, [5s]) (Long Breath, Operation, [1.2s]) (Long Breath, Wait, [2.8s]) (Decide, Wait, [1s]) (1 st Info, Receive, [5s]) 2) (Decide, Init, [1s]) (1 st Info, Receive, [5s]) (Short Breath, Operation, [1.2s]) (Finish, Finish, [ ]) 3) (Decide, Init, [1s]) (1 st Info, Receive, [5s]) (Short Breath, Operation, [1.2s]) (Short Breath, Wait, [0.8s]) (2 nd Info, Receive, [5s]) (Long Breath, Operation, [1.2s]) (Finish, Finish, [ ]) 4) (Decide, Init, [1s]) (1 st Info, Init, [4s]) (Fail, Fail, [ ]) 5) (Decide, Init, [1s]) (1 st Info, Receive, [5s]) (Short Breath, Operation, [1.2s]) (Short Breath, Wait, [0.8s]) (2 nd Info, Receive, [5s]) (Long Breath, Operation, [1.2s]) (Long Breath, Wait, [2.8s]) (Decide, Wait, [1s]) (Fail, Fail, [ ]) 6) (Decide, Init, [1s]) (1 st Info, Receive, [5s]) (Short Breath, Operation, [1.2s]) (Short Breath, Wait, [0.8s]) (2 nd Info, Wait, [3s]) (Fail, Fail, [ ]) 위시퀀스는크게 3가지의경우로나타낼수있다. 1) 번시퀀스는계속적으로음성정보에의해관제가이루어지는경우이고, 2) 번과 3) 번은결심고도에도달하여 PAR 관제를종료하는경우이고, 4) 번부터 6) 번까지는 5 초간지속적인음성정보가제공되지않아통신두절이발생하여 PAR 관제가실패한경우이다. 모든상태시퀀스에서시스템의안전성과필연성을살펴보면, 종료조건을제외하고무한대의시간을가지는상태는존재하지않으므로데드락이없고, 언젠가는성공또는실패상태에도달하게되므로라이브락또한없다. 그러므로기존시스템은안전성과필연성을만족하는시스템이다. 5.2 제안하는디지털정보에의한관제제안하는디지털정보에의한관제모델과조종사모델의합성은그림 9와같이나타난다. 초기에 (Send, Init) 상태에서메시지를받으며상태가변하며, (Send, Operation) 상태에서결심고도에도달하게되면 (Finish, Finish) 상태에서종료하거나계속적으로 (Send, Wait) 상태를반복하며관제신호를모니터링하고조종한다. 음성신호에의한관제와마찬가지로통신상태이상으로모니터에관제신호가수신되지않을시 (!command, ) 와같은이벤트가발생하고, 5초동안문제가발생시 (Fail, Fail) 상태로이동한다. 이때조종사의조종으로인해바뀌는항공기의정보는관제시스템의모니터로항상수신되며이정보는누수되지않는것으로가정한다. 즉, 6 한국시뮬레이션학회논문지
DEVS 형식론을이용한공항 PAR 관제시스템자동화방안검증 그림 8. 기존의음성을이용하는관제프로토콜의 C-DEVS 모델 1) (Send, Init, [2.5s]) (Send, Operation, [1.2s]) (Send, Wait, [1.3s]) (Send, Operation, [1.2s]) 2) (Send, Init, [2.5s]) (Send, Operation, [1.2s]) (Send, Wait, [1.3s]) (Send, Wait, [2.5s]) (Send, Operation, [1.2s]) 3) (Send, Init, [2.5s]) (Send, Init, [2.5s]) (Send, Operation, [1.2s]) 4) (Send, Operation, [1.2s]) (Finish, Finish, [ ]) 5) (Send, Init, [2.5s]) (Send, Operation, [1.2s]) (Send, Wait, [1.3s]) (Send, Wait, [2.5s]) (Fail, Fail, [ ]) 6) (Send, Init, [2.5s]) (Send, Init, [2.5s]) (Fail, Fail, [ ]) 그림 9. 제안하는프로토콜의 C-DEVS 모델 : 디지털정보에의한관제모델과조종사모델의합성 조종사로부터관제시스템으로오는메시지는손실없이모두전달된다. 제안하는시스템프로토콜의전체상태시퀀스는다음과같다. 위시퀀스는다음과같이분류할수있다. 1) 번은지속적인디지털관제정보송수신으로통신두절없이 PAR 관제가반복적으로이루어지는경우이고, 2) 번과 3) 번은한번의통신두절은일어났지만 5초이내이기때문에지속적인관제가이루어지는경우이다. 4) 번은결심고도에도달하여 PAR 관제가완료된경우이며, 5) 번과 6) 번은 5 초이상의통신두절로인해 PAR 관제가실패한경우이다. 제안하는시스템의안전성과필연성을살펴보면, 이시스템또한데드락과라이브락이존재하지않는것을확인할수있다. 그러므로제안하는시스템은안전성과필연 제 21 권제 3 호 2012 년 9 월 7
성창호 구정 김탁곤 김기형 표 1. 두시스템의상태시퀀스검증결과 분류 음성관제 디지털관제 결과 관제지속 1) 1) 2) 3) 동일 관제성공 2) 3) 4) 동일 관제실패 4) 5) 6) 5) 6) 동일 성을만족하는시스템이다. 5.3 시스템검증제안하는 PAR 자동화시스템이기존의음성에의한관제와동일한기능을수행하는지검증하기위해앞에서얻은전체상태시퀀스를비교한다. 우선반복되는시퀀스로서음성 C-DEVS 모델의 1) 번과디지털 C-DEVS 모델의 1) 번, 2) 번, 3) 번이의미적으로동일하다. 디지털모델의경우통신두절이한번발생하더라도 5초이내에한번더보낼수있으므로여러개의시퀀스가존재하고지속적인관제가가능하다. 그리고음성모델의 2) 번, 3) 번과디지털모델의 4) 번시퀀스는 PAR 관제가성공하는시퀀스로서동일하다. 음성모델은음성정보를두번나누어서보내므로두개의시퀀스가나올수있다. 마지막으로 5초이상의통신두절에의해 PAR 관제가실패하는경우가음성모델의 4) 번, 5) 번, 6) 번과디지털모델의 5) 번, 6) 번이다. 표 1은검증결과를요약한것이다. 6. 결론 본논문은자동화된공항 PAR 관제시스템을제안하고이를 DEVS 형식론을이용하여검증하는것이다. PAR 관제의효율성을위하여디지털신호를이용한자동화방안을제안하고그동작을기존의음성신호에의한관제시스템과비교하였다. 시스템의기능검증을위하여확장된 DEVS 형식론인 C-DEVS 형식론을이용하고, 모든상태시퀀스를검증한결과제안하는시스템이기존시스템과동일하게동작함을확인하였다. C-DEVS 형식론을이용한기능검증및분석은실제시스템을구축하기에앞서수학적인모델을이용함으로써모든상황에대한검증을가능하게하며, 이를통해시스템개발의안전성및경제성을높일수있다. 본논문에서언급되어있는항공기관제시스템의경우처럼, 실체계에바로적용하여테스트하기어려운경우 C-DEVS 모델검증방법론이유용하게사용될수있다. 본논문에서제안하는디지털신호에의한관제는청 각정보가아닌시각정보를사용함으로써정보전달의정확성을높여줄것으로기대되며, 향후실제항공기의파라미터를이용하여제안하는시스템의성능을측정하기위한연구가필요하다. 참고문헌 1. 공군본부, 공교 3-143 국지계기절차수립기준, 2007.1.1. 공 2. 공군작전사령부, 비행정보간행물, 2010.4.16. 3. FAA, Aeronautical Information Manual, February, 9. 2012. 4. 구정, 표상호, 강경성, 김기형, 재래식주파수도약통신장비용 S/W 패킷모뎀개발및적용에관한연구, 한국군사과학기술학회지 ( 통권 51 호 ), pp. 222-231, 2011. 4. 5. 구정, 표상호, 강경성, 김기형, 비행기지 PAR 을이용한 DGPS 공항접근및착륙정확도분석, 한국군사과학기술학회지 ( 통권 54 호 ), pp. 788-797, 2011.10. 6. B. P. Zeigler, T. G. Kim, and H. Praehofer, Theory of Modeling and Simulation, Orlando, FL: Academic, 2000. 7. 공군본부, 내트워크중심작전사례연구 ( Link-16 유 / 무시의공대공전투 ), 2010. 8. 8. J. Miller, Channel interaction and the redundant-targets effect in bimodal divided attention, Journal of Experimental Psychology: Human Perception and Performance, Vol. 17, pp. 160-169, Feb. 1991. 9. D. W. Massaro and D. S. Warner, Dividing attention between auditory and visual perception, Perception & Psychophysics 21, pp. 569-574, 1977. 10. W. B. Lee and T. G. Kim, Ordering Method for Reducing State Space in Compositional Verification, in 1999 IEEE International Conference on Systems, Man, and Cybernetics (IEEE SMC 99), Tokyo, Japan, pp. I-806 - I-811, Oct. 1999. 11. T. G. Kim, DEVS Formalism for Modeling of Discrete-Event Systems, Handbook of Dynamic System Modeling (ED. P. A. Fishwick), Chapman & Hall/CRC, Ch. 6, pp. 6-1 6-13, May 2007. 12. L. Lamport, Proving the Correctness of Multiprocess Programs, IEEE Trans. Softw. Eng. Vol. 3, No. 2, pp. 125-143, Mar. 1977. 13. B. Alpern, F. B. Schneider, Defining liveness, Information Processing Letters, Vol. 21, Issue 4, pp. 181-185, Oct. 1985. 14. 공군본부, 공교 3-9-2/ 표준계기비행, 2012.1.2. 15. FAA, FAA-H-8380-15A Instrument Flying Handbook, 2008. 16. 공군본부, 공교 3-2-8/ 작전항공교통관제절차, 2012.1.1. 8 한국시뮬레이션학회논문지
DEVS 형식론을이용한공항 PAR 관제시스템자동화방안검증 성창호 (chsung@smslab.kaist.ac.kr) 2003 부산대학교전자전기통신공학부학사 2011 KAIST 전기및전자공학과박사 2011~ 현재 KAIST 정보전자연구소연수연구원 관심분야 : 모델링 / 시뮬레이션이론, 분산및하이브리드시뮬레이션 구정 (hanair9@hanmail.net) 1982 공군사관학교항공공학학사 1993 인하대학교항공공학석사 2011 NCW협동공학박사과정수료 2002~2003 공군전투발전단모의체계과장 2004~2005 공군전투발전단모의분석과장 2007~2008 합동참모본부워게임운영과장 2009~2010 공군본부정보화기획실체계관리처장 2010~ 공군작전정보통신단장 관심분야 : NCW, 항공전자, Data Link, M&S, 전투실험 김탁곤 (tkim@ee.kaist.ac.kr) 1975 부산대학교전자공학과학사 1980 경북대학교전자공학과석사 1988 Univ. of. Arizona, 전기및컴퓨터공학과박사 1980~1983 부경대학교, 통신공학과, 전임강사 1987~1989 ( 미 ) 아리조나환경연구소, 연구엔지니어 1989~1991 Univ. of Kansas, 전기및컴퓨터공학과, 조교수 1991~현재 KAIST 전기및전자공학과, 교수 - 한국시뮬레이션학회회장역임 - 국제시뮬레이션학회 (SCS) 논문지 (Simulation) Editor-In-Chief 역임 - SCS Fellow - 모델링시뮬레이션기술사 ( 미국 ) - Who s Who in the World(Marguis 16thEdition, 1999) 등재 - 연합사, 국방부 / 합참, 기품원자문위원역임 - KIDA Fellow 역임 - ADD 자문위원 ( 현 ) 관심분야 : 모델링 / 시뮬레이션이론, 방법론및환경개발, 시뮬레이터연동 김기형 (kkim86@gmail.com) 1990 한양대학교전자통신공학과학사 1992 한국과학기술원전자공학과석사 1996 한국과학기술원전자공학과박사 1997. 3~2005. 2 영남대학교컴퓨터공학과, 부교수 2000.12~2001. 8 AdForce, Inc (California Cupertino), Senior Engineer 2005. 3~ 현재아주대학교, 교수 2011. 9~2012. 8 Stony Brook University (State University of New York), Visiting Professor 관심분야 : M2M, ISA100, wirelesshart, 6LoWPAN, wireless sensor networks, mobile embedded systems, 전술네트워크 제 21 권제 3 호 2012 년 9 월 9