닫기
Loading..

전자정보연구정보센터 ICT 융합 전문연구정보의 집대성

국내 논문지

홈 홈 > 연구문헌 > 국내 논문지 > 한국정보과학회 논문지 > 정보과학회논문지 (Journal of KIISE)

정보과학회논문지 (Journal of KIISE)

Current Result Document : 10 / 15 이전건 이전건   다음건 다음건

한글제목(Korean Title) FMProjector: 표준 인터페이스를 준수하는 운영체제를 위한 정형 검증 프레임워크
영문제목(English Title) FMProjector: A Formal Verification Framework for an Operating System Complying with a Standard Interface
저자(Author) 이동아   유준범   Dong-Ah Lee   Junbeom Yoo  
원문수록처(Citation) VOL 46 NO. 08 PP. 0814 ~ 0822 (2019. 08)
한글내용
(Korean Abstract)
정형 검증은 소프트웨어의 정확성을 검증할 수 있는 유용한 기법이지만, 운영체제와 같이 규모가 큰 소프트웨어 전체를 대상으로 한번에 적용하는 것에는 상태 폭발같은 문제로 인해 어려움이 따른다. IEC 61508이나 DO-178과 같은 안전 필수 분야의 표준에서는 정형 검증을 통한 소프트웨어의 정확성 확인을 소프트웨어의 안전 수준에 따라 일부 권장하고 있다. 본 논문에서는 표준 인터페이스를 준수하는 운영체제를 위한 정형 검증 프레임워크, FMProjector를 소개한다. 운영체제를 검증하기 위하여 소프트웨어를 수평적·수직적으로 분석하기 위한 접근 방법을 제안하며, 표준 인터페이스로부터 운영체제의 모든 개발산출물에 대한 추적성을 기반으로 검증 영역을 식별할 수 있는 체계적인 방법을 제시한다. FMProjector를 항공용 RTOS의 인터페이스 표준인 ARINC-653을 준수하도록 개발한 운영체제, Qplus-AIR를 대상으로 적용한 사례연구를 소개한다.
영문내용
(English Abstract)
Formal verification techniques facilitate the verification of functional correctness of software. The verification, however, is rarely applicable to large-scale software, such as operating systems, because of the state explosion problem. International standards or certifications, such as IEC-61508 or DO-178, highly recommend formal verification of such software according to the level of safety. The paper introduces a formal verification framework, FMProjector, for operating systems complying with a standard interface. The framework includes horizontal and vertical approaches for systematic analysis of the software based on traceability from the standard interface to the source code. The paper also introduces a case study for the application of FMProjector to Qplus-AIR complying with ARINC-653 which is a standard interface for avionics real-time operating system.
키워드(Keyword) 정형 검증   운영체제   추적성분석   표준 인터페이스   formal verification   operating system   traceability analysis   standard interface  
원문 PDF 다운로드