Esterel을 이용한 마이크로커널 시스템 정형 검증 (Formal Verification of Microkernel-based Operating System using Esterel)

서지정보

· 발행기관 : 한국정보기술학회
· 수록지 정보 : 한국정보기술학회논문지 / 6권 / 3호 / 75 ~ 82페이지
· 저자명 : 이수영, 방기석, 고영웅

초록

마이크로커널 기반 운영체제는 마이크로커널, 응용 프로그램 그리고 운영체제 서버 등이 프로세스간 통신을 통하여 동적으로 수행되기 때문에 수행 과정에 있어서의 정확성을 검증하기 매우 어렵다. 시스템의 정확성을 검증하기 위한 방법으로 설계 및 구현단계에서 전통적으로 사용되는 테스팅(testing) 기법 등을 활용하는 것으로 충분하지 않다. 본 논문에서는 마이크로커널 기반 운영체제에 대해서 정형 기법을 적용하여 이러한 문제를 해결하고자 시도하였다. 본 연구의 목적을 달성하기 위해서 마이크로커널 기반 시스템의 내적/외적으로 발생하는 다양한 이벤트의 동작에 대해서 초점을 맞추어 모델링을 하였다. 그리고 정형 기법 도구로 널리 알려져 있는 Esterel을 이용하여 안전성을 검증하는 작업을 수행하였다. 본 논문에서는 Esterel로 동기적 시스템 설계에 대한 정확한 행위를 검사할 수 있었으며, 마이크로커널 기반 운영체제 시스템 검증에 효과적으로 사용될 수 있음을 보였다.

영어초록

Microkernel-based operating systems are known to be difficult to predict their behavioral correctness since the microkernel communicates with various components(microkernel, application and OS server) for their execution. That means its correctness is not easy to guarantee by using traditional design and testing methods. In this paper, we propose a formal verification method for microkernel-based operating systems. To accomplish our goal, we first extract a formal model of the systems focusing on the behavior of system services representing internal and external events. Then we verify the proposed model whether they meet our safety properties using well-known model checking tools(Esterel). With Esterel, we can examine the correct behavior of a synchronous system design. Our conclusion is that model checking is an effective means of improving the quality of microkernel-based systems at scale.

참고자료

· 없음