[논문]정형검증 도구를 활용한 Fly-By-Wire 헬리콥터 비행제어법칙 자동코드 무결성 확보 방안

안성준; 조인제; 강혜진

doi:10.5139/jksas.2014.42.5.398

정형검증 도구를 활용한 Fly-By-Wire 헬리콥터 비행제어법칙 자동코드 무결성 확보 방안
Secure methodology of the Autocode integrity for the Helicopter Fly-By-Wire Control Law using formal verification tool 원문보기

한국항공우주학회지 = Journal of the Korean Society for Aeronautical & Space Sciences, v.42 no.5, 2014년, pp.398 - 405

안성준 (Korea Aerospace Industries) , 조인제 (Korea Aerospace Industries) , 강혜진 (APPIA Engineering)

초록
AI-Helper

내장형 소프트웨어 기술이 항공 및 방위산업과 같은 안전-필수 시스템에 적용됨에 따라 보다 높은 소프트웨어의 신뢰성이 요구되고 있다. 그 중에서 소프트웨어의 무결성은 주로 정적 분석 도구를 이용해 검증이 이뤄지고 있으며 최근에 개발된 정적 분석 도구는 수학적인 분석 방법을 통해 코드의 무결성을 평가하고 있다. 본 연구에서는 정형 검증 도구인 Polyspace를 이용해 자동코드의 결함을 검출하고, 코딩규칙의 준수 여부를 검증하였다. 검증된 결과를 바탕으로 결함을 가진 제어법칙 모델을 수정하여 코드 생성 이전의 원천적인 결함을 제거 가능함을 확인하였고 FBW 헬리콥터 제어법칙 자동생성코드의 무결성을 확보 할 수 있었다.

Abstract ▼ AI-Helper

Recently the embedded software has been widely applied to the safety-critical systems in aviation and defense industries, therefore, the higher level of reliability, availability and fault tolerance has become a key factor for its implementation into the systems. The integrity of the software can be verified using the static analysis tools. And recent developed static analysis tool can evaluate code integrity through the mathematical analysis method. In this paper we detect the autocode error and violation of coding rules using the formal verification tool, Polyspace(R). And the fundamental errors on the flight control law model have been detected and corrected using the formal verification results. As a result of verification process, FBW helicopter control law autocode can ensure code integrity.

주제어

AI 본문요약
AI-Helper

* AI 자동 식별 결과로 적합하지 않은 문장이 있을 수 있으니, 이용에 유의하시기 바랍니다.

문제 정의

회색은 한 번도 실행될 수 없는 데드코드를 의미하며 주황색은 런타임 오류를 발생시킬 가능성이 포함되어있는 코드이다. 녹색을 제외한 색상의 코드에 대하여 어떤 종류의 런타임 오류가 발생하는지에 대하여 보고한다. FBW 헬리콥터 제어법칙 자동 코드에서 몇 가지 회색 코드와 주황색 코드가 발생하였다.
본 논문에서는 MATLAB/SIMULINK로 설계한 Fly-By-Wire 헬리콥터 제어법칙 모델에서 생성된 코드의 코딩규칙과 무결성을 확보하기 위하여 상용 정적 분석 도구를 이용한 검증 프로세스를 제안하였다. 그리고 제안된 프로세스를 통해 자동생성코드를 검증하여 소스코드에 잠정적인 오류를 파악하고, 발생된 오류를 제거해 자동생성코드의 무결성을 확보하는 방법을 제안하였다.
그러기 위해서는 자동생성코드에 대한 무결성을 개발초기에 확보하는 것이 중요하다. 본 논문에서는 Simulink에서 생성된 자동생성코드를 상용 검증 도구인 Polyspace라는 정형 기법과 결합된 정적 분석 도구를 사용하여 검증절차와 그 검증절차를 따른 무결성 확보 방안을 제시하였다.
정형 기법 중 정형 검증의 가장 대표적인 해석방법은 추상적 해석이며, 이 방법은 런타임 오류가 없음을 증명하는 수학적으로 뛰어난 접근방식이다. 이 해석법은 코드의 각 상태를 분석하는 대신 이러한 상태를 보다 일반적인 형태로 표현 하고 그것을 조작할 수 있는 규칙을 제공해준다. 예를 들어 소스코드 내의 변수의 모든 범위를 확인한 뒤 Division by Zero(ZDV) 오류가 있는지 Fig.

제안 방법

1. 런타임 오류 검증
검증도구를 이용하여 개발 초기에 소스코드에 런타임 오류의 존재여부를 검증하고, 코딩규칙 준수여부를 검사한다. 소스코드를 검사하여 잠재적인 결함이 발생 할 수 있는 부분을 파악하여 각 라인별 코드의 상태를 색상으로 구분하여 준다.
분석된 부분은 제어법칙 가이드라인에 반영이 되고 제어법칙 모델의 수정이 이루어진다. 그 결과를 바탕으로 다시 모델검증이 이루어지고, 이 과정을 런타임 오류가 검출되지 않을 때까지 반복적으로 수행하여 자동생성코드의 무결성을 검증한다.
1의 붉은 선과 같이 검사하며 +표시는 변수가 가질 수 있는 모든 가능 범위를 나타낸 것이다. 그 다음 모든 가능 범위에 대하여 if-else, for loop 또는 while loop, switch, inter-procedural operations (function calls)분석에 걸릴 데이터 간의 관계를 표현하기 위해 다면체로 나누며 이것을 기반으로 코드를 분석한다[8].
본 논문에서는 MATLAB/SIMULINK로 설계한 Fly-By-Wire 헬리콥터 제어법칙 모델에서 생성된 코드의 코딩규칙과 무결성을 확보하기 위하여 상용 정적 분석 도구를 이용한 검증 프로세스를 제안하였다. 그리고 제안된 프로세스를 통해 자동생성코드를 검증하여 소스코드에 잠정적인 오류를 파악하고, 발생된 오류를 제거해 자동생성코드의 무결성을 확보하는 방법을 제안하였다.
먼저 모델에서 생성된 자동코드를 상용검증도구를 이용하여 런타임 오류가 있는지 분석한다. 런타임 오류가 검출되면 발생한 문제에 대하여 개발자에게 보고하고, 보고된 결과를 바탕으로 검증도구 내부의 문제인지 제어법칙 모델의 설계결함 인지를 파악 하는 분석 과정을 거친다. 분석된 부분은 제어법칙 가이드라인에 반영이 되고 제어법칙 모델의 수정이 이루어진다.
2와 같다. 먼저 모델에서 생성된 자동코드를 상용검증도구를 이용하여 런타임 오류가 있는지 분석한다. 런타임 오류가 검출되면 발생한 문제에 대하여 개발자에게 보고하고, 보고된 결과를 바탕으로 검증도구 내부의 문제인지 제어법칙 모델의 설계결함 인지를 파악 하는 분석 과정을 거친다.
본 과제에서 코딩규칙 준수를 위해 모델의 옵션 중 괄호설정과 관련된 부분이 수정되었으며, 다양한 장비와 인터페이스를 위해서 작성된 Custom Template File에서 모델의 정보를 받아와 외부와 인터페이스 할 수 있도록 생성된 wrapper file역시 코딩규칙을 준수를 위해 함수 선언부분을 수정하였다. 단 C에서 지원하지 않는 Boolean 형태의 변수와 Logical Operator를 사용함으로 인하여 코딩규칙 위반이 발생하였으며 이 문제는 공용함수 블록의 알고리즘을 변경하여 해결할 예정이다.
본 논문에서는 정형검증(Formal Verification) 중의 추상적 해석(Abstract interpretation)알고리즘을 이용한 정형검증도구를 이용하여 무결성 검증을 수행하였다.
검증도구를 이용하여 개발 초기에 소스코드에 런타임 오류의 존재여부를 검증하고, 코딩규칙 준수여부를 검사한다. 소스코드를 검사하여 잠재적인 결함이 발생 할 수 있는 부분을 파악하여 각 라인별 코드의 상태를 색상으로 구분하여 준다. 개발자는 검증결과를 바탕으로 오류를 일으킬 가능성이 있는 코드에만 집중할 수 있으므로 검증 시간이 단축될 수 있다.
5와 같이 모델에 사용되는 스위치블록의 입력 값이 Ground 블록을 사용함으로써 회색코드가 발생하게 되었다. 이 문제를 해결하기 위해 Fig. 6과 같이 Ground 블록을 제거하고 최상위 블록까지 입력포트를 연결하여 회색코드를 제거 하였다.

대상 데이터

클라이언트는 서버로부터 검증 결과를 받아 확인하는데 이 때 자신이 요청한 검증만 다운로드 받을 수 있다. 본 검증에서는 클라이언트 2대, 서버 1대를 이용하여 Fig. 3과 같이 구성하였다. 클라이언트1이 서버로 큐 매니저를 통해 검증 요청한 것은 클라이언트 1만 결과를 다운받아 확인가능하며 클라이언트 2는 확인해볼 수 없다.

이론/모형

FBW 헬리콥터 코딩규칙은 MISRA AC AGC코딩규칙과 참조항공기 코딩규칙을 적용하여 선정하였다. FBW 헬리콥터의 코딩규칙은 참조항공기 탑재비행제어 소프트웨어 개발에 사용되었던 코딩 규칙을 기본으로 하여 MISRA AC AGC규칙중 off된 규칙을 적용하여 만들어 졌다.

성능/효과

검증 결과는 녹색(Green Code), 적색(Red Code), 회색(Gray Code), 주황색((Orange Code)으로 색상은 표시되며 녹색은 런타임 오류가 없는 안전한 코드이고 적색은 런타임 오류가 발생하는 코드이다. 회색은 한 번도 실행될 수 없는 데드코드를 의미하며 주황색은 런타임 오류를 발생시킬 가능성이 포함되어있는 코드이다.
7과 같이 (-)연산 우측의 제어법칙 입력변수에서 발생하였다. 검증도구에서 지원하는 Data Range Specifications (DRS)라는 기능을 자동 검증 도구의 옵션에 추가하여 오버플로우를 발생시키는 변수의 실행 범위를 지정해 줌으로써 검증도구에 추가적인 정보를 제공하여 런타임 오류가 발생하지 않음을 증명할 수 있었다.

후속연구

코딩 규칙위반에 대해서는 공용함수 알고리즘을 변경할 예정이다. FBW 헬리콥터 제어법칙 모델의형상이 확정될 때까지 자동코드에 대한 검증을 계속 하여 100%의 코드 무결성을 확보할 예정이다.
본 과제에서 코딩규칙 준수를 위해 모델의 옵션 중 괄호설정과 관련된 부분이 수정되었으며, 다양한 장비와 인터페이스를 위해서 작성된 Custom Template File에서 모델의 정보를 받아와 외부와 인터페이스 할 수 있도록 생성된 wrapper file역시 코딩규칙을 준수를 위해 함수 선언부분을 수정하였다. 단 C에서 지원하지 않는 Boolean 형태의 변수와 Logical Operator를 사용함으로 인하여 코딩규칙 위반이 발생하였으며 이 문제는 공용함수 블록의 알고리즘을 변경하여 해결할 예정이다.
4%의 무결성을 만족 하였고, 코딩규칙에관련해선 위에서 언급한 Boolean과 Logic Operator에 의한 2개의 규칙위반을 제외한 나머지 부분은 만족 하는 것을 확인 할 수 있었다. 위에서 발생한 런타임 오류를 해결하기 위하여 개발회사와 협조하고 있으며, 추가적인 알고리즘 변경으로 해결될 예정이다. 코딩 규칙위반에 대해서는 공용함수 알고리즘을 변경할 예정이다.
이와 같은 문제는 모델 가이드라인을 따라서 모델이 개발되었다면 자동생성코드 검증단계까지 진행되기 이전에 수정될 수 있는 문제로써 향후 제어법칙 모델 개발 시 설계단계에서 다양한 방법으로 모델검증을 수행할 예정이다.
이러한 입력에 대한 간단한 오버플로우 결함은 제어법칙 내부의 리미터로 예방할 수 있는 문제이고 좀 더 원천적인 문제를 해결할 수 있는 방법으로 판단된다. 좀 더 복잡한 로직 수행 시 발생할 수 있는 오버플로우 결함에 대한 연구가 필요하다.
현재 Fly-By-Wire 헬리콥터 제어법칙 자동생성 코드 개발에 적용하고 있으며, 결함을 수정한 모델과 코드에 대한 검증이 이루어지고 있으며 모델의 개발 완료까지 런타임 환경에서의 검출 가능한 모든 오류를 자동코드생성 가이드라인과 검증도구를 통해 제거한다면 보다 효율적인 자동생성코드의 무결성을 확보할 수 있을 것이라 판단된다.

질의응답

핵심어	질문	논문에서 추출한 답변
	정적 분석이란 무엇인가	정적 분석(Static Analysis)은 프로그램을 컴파일하고 실행하기 전에 소스 코드 수준의 어휘, 구문 분석을 통한 문법 구조를 분석하여 소스코드의 정보를 얻어내는 것을 말한다. 정적 분석은 전형적인 결함 이외에 구제적인 특정 변수 값 대신에 추론 가능한 모든 변수의 값을 사용하는 방식을 사용하기도 한다[3]
	정형기법의 목적은 무엇인가	정형기법(Formal Method)은 소프트웨어 공학의 해석 기법의 일종으로 오류가 없는 시스템을 설계하여 시스템의 신뢰성을 높이는데 목적이 있다. 요구명세 및 설계명세를 모두 수학적인 문자나 기호로 명세하여 수학적인 증명 방법으로 설계된 시스템의 다양한 특성 및 신뢰성을 검증하고 있다[5].
	항공 및 방위 산업에 적용되는 소프트웨어의 신뢰성을 얻는 방법은 무엇인가	항공 및 방위 산업에 적용되는 소프트웨어에서 발생하는 결함은 인명 피해를 초래하기 때문에 신뢰성 평가가 매우 중요하다[1]. 신뢰성을 얻기 위한 방법 중 하나로 정적분석이 수행된다. 이 분석 방식은 코드 내부의 잠재적인 오류가 있는지 확인 할 수 있는 방법이며, 보통 상용 정적분석 도구를 이용해 이루어진다.

참고문헌 (8)

Ki-Du Kim, A Study on Reliability Evaluation for Embedded Software, The Institute of Internet, Broadcasting and Communications, Vol.9, No.3, 2009
Sung-jin Park, Preparation for dynamic testing and failure detection of Safety-cretical software using a Advanced static analysis tool, Embeddedworld, No.11, 2010
Seung-Hwa Song, Graphical Presentation Model for Static Analysis of Software, Korea Computer Congress, Vol.34, No.1, 2007
Won-Il Gwun,Practical Software Testing Foundation, STA Consulting Inc., 2010
John Rushby, Formal Method and the certification of Critical Systems, Technical Report CSL-93-7, SRI International, Menro Park, CA, 1993
Chang-Hun Sung, Development Methodology of Safety-Critical System Using Formal Method, Vol.27. No.2 , 2000
P.Cousot, Formal Verification by Abstract interpretation, 4th NASA Formal Methods Symposium(NFM2012), Lecture Notes in Computer Science Volume 7226, 2012, pp 3-7
Code Verification and Run-Time Error Detection Through Abstract Interpretation, white paper, mathworks

표제어: PCR

동의어: Packet Collision Rate

용어 설명 출처 목록 (6)

용어 설명: PCR은 세균 특이성이 있는 primer를 이용하여 적은 수의 세균이 있을지라도 쉽게 검출할 수 있는 유용한 방법이며, 이를 이용하여 구강 내 치면세균막이나 타액에서 직접 세균을 검출할 수 있게 되었다[8].

내보내기 구분	파일저장 인쇄 메일전송
구성항목	기본정보 상세정보 관리번호, 논문명, 저널/프로시딩명, 저자 , 발행년, 권, 호, 시작페이지, 끝페이지, 발행기관 관리번호, 논문명, 대등논문명, 저자 , 저널/프로시딩명, 발행기관, 발행년, 발행언어, 권, 호, 시작페이지, 끝페이지, ISBN, ISSN, 주제분야, 키워드, 초록(한글), 초록(영문), 저자(소속기관)
저장형식	Text(ASCII format) Excel format RefWorks Direct Export RIS format (for Reference Manager, ProCite, EndNote), Scholar's Aids, Mendeley
메일정보	받는사람 (필수) @ 보내는사람 (선택) @ 제목 내용 KISTI 검색결과 이메일 서비스
안내	총 건의 자료가 검색되었습니다. 다운받으실 자료의 인덱스를 입력하세요. (1-10,000) 검색결과의 순서대로 최대 10,000건 까지 다운로드가 가능합니다. 데이타가 많을 경우 속도가 느려질 수 있습니다.(최대 2~3분 소요) 다운로드 파일은 UTF-8 형태로 저장됩니다. 파일의 내용이 제대로 보이지 않을실 때는 웹브라우저 상단의 보기 -> 인코딩 -> 자동선택 여부를 확인하십시오. ~ Text(ASCII format) Excel format

연합인증

정형검증 도구를 활용한 Fly-By-Wire 헬리콥터 비행제어법칙 자동코드 무결성 확보 방안
Secure methodology of the Autocode integrity for the Helicopter Fly-By-Wire Control Law using formal verification tool 원문보기

초록
AI-Helper

Abstract ▼ AI-Helper

주제어

AI 본문요약
AI-Helper

문제 정의

제안 방법

대상 데이터

이론/모형

성능/효과

후속연구

질의응답

참고문헌 (8)

이 논문을 인용한 문헌

관련 콘텐츠

원문 보기

원문 URL 링크

이 논문과 함께 이용한 콘텐츠

AI-Helper ※ AI-Helper는 오픈소스 모델을 사용합니다.

선택된 텍스트

연합인증

정형검증 도구를 활용한 Fly-By-Wire 헬리콥터 비행제어법칙 자동코드 무결성 확보 방안 Secure methodology of the Autocode integrity for the Helicopter Fly-By-Wire Control Law using formal verification tool 원문보기

초록 용어보기논문에서 용어와 풀이말을 자동 추출한 결과로, 시범 서비스 중입니다. AI-Helper

Abstract ▼ AI-Helper

주제어

AI 본문요약 엑셀 다운로드 AI-Helper

문제 정의

제안 방법

대상 데이터

이론/모형

성능/효과

후속연구

질의응답

참고문헌 (8)

이 논문을 인용한 문헌

관련 콘텐츠

원문 보기

원문 URL 링크

이 논문과 함께 이용한 콘텐츠

AI-Helper ※ AI-Helper는 오픈소스 모델을 사용합니다.

선택된 텍스트

정형검증 도구를 활용한 Fly-By-Wire 헬리콥터 비행제어법칙 자동코드 무결성 확보 방안
Secure methodology of the Autocode integrity for the Helicopter Fly-By-Wire Control Law using formal verification tool 원문보기

초록
AI-Helper

AI 본문요약
AI-Helper