검증 반례 재연을 통한 모델 기반 커널 테스팅

Abstract

최근 내장 시스템의 용도에 따라 이에 적합한 운영체제 커널을 제작하고자 하는 요구가 증가되고 있다. 하지만 커널 개발은 코드의 복잡성, 유닛 테스팅의 어려움, 동시성으로 인한 동작 경우의 수 증가, 적합한 툴의 부재 등의 이유로 인해 아직도 개발 및 테스팅 비용이 큰 실정이다. 이러한 커널 개발 및 테스팅의 어려움을 극복하기 위해, 모델 기반의 커널테스팅 (MOKERT) 프레임워크를 제안한다. 본 프레임워크는 모델 검증 기법과 테스팅 기법을 조합하여 운영체제 커널 내의 동시성 오류 검출을 지원한다. 본 연구에서는 검증하고자 하는 리눅스 2.6 커널의 파일시스템 구성요소에 MOKERT 프레임워크를 적용하여 이의 효율성을 증명하였다.