우선순위 기반 멀티태스크 프로그램의 API 호출 안전성 검증을 위한 모델 기반 오경보 식별 기법

김동우; 최윤자; Dongwoo Kim; Yunja Choi

연구문헌

국내 논문지

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

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

Current Result Document : 3 / 6 이전건 다음건

한글제목(Korean Title)	우선순위 기반 멀티태스크 프로그램의 API 호출 안전성 검증을 위한 모델 기반 오경보 식별 기법
영문제목(English Title)	False-alarm Detection in Model-based API-call Safety Checking of Priority-based Multitasking Programs
저자(Author)	김동우 최윤자 Dongwoo Kim Yunja Choi
원문수록처(Citation)	VOL 46 NO. 10 PP. 1035 ~ 1043 (2019. 10)
한글내용 (Korean Abstract)	멀티태스크 프로그램은 다수의 태스크가 운영체제의 스케줄링에 맞추어 번갈아 수행되는 프로그램이다. 멀티태스크 프로그램을 검증하기 위해서는 운영체제의 행위를 고려해야하며 그렇지 않을 경우 우선순위가 낮은 태스크가 먼저 실행되는 등 오경보가 발생한다. 효과적인 멀티태스크 프로그램 검증을 위해 정형 운영체제 모델을 사용한 모델 검증 방법들이 소개되었으나 이들은 프로그램을 추상화함으로 인해 오경보를 보고할 수 있다는 단점이 있다. 본 연구에서는 모델 검증 결과 보고된 반례의 오경보 여부를 식별하기 위하여 반례와 동일한 순서로 API 함수 호출을 수행하는 프로그램 실행 경로의 존재 여부를 코드검증 기법을 이용하여 확인하는 방법을 소개한다. 본 연구의 효과를 입증하기 위해 차량전장용 운영체제를 위한 테스트 프로그램과 차량전장용 창문 제어 프로그램을 검증하고 보고된 반례의 오경보 여부를 식별한 결과 73%는 오경보임을 확인하였으며 각각 평균 0.199초와 17.95초의 식별 시간이 소요되었다.
영문내용 (English Abstract)	A multitask program consists of a set of tasks that are executed according to a scheduling policy of the operating system. In order to verify a multitask program, it is necessary to consider the behavior of the operating system. Otherwise, false alarms are reported, e.g., a low-priority task is executed prior to a higher-priority task. Studies introduced a model-based verification method using the formal OS model for the effective verification of multitask programs, but they showed high false-alarm rates due to the abstraction of the application program. This paper proposes an automated false-alarm detection method which identifies false alarms by checking existence of the program path that performs the same sequence of API-calls as the counterexample reported by the model-based verification. The suggested method is applied to two sets of application programs running on an automotive operating system. Results show that 73% of the reported counterexamples were false alarms with an average detection time of 0.199 seconds for the test program and 17.95 seconds for the window control program.
키워드(Keyword)	API API 호출 제약사항 검증 정형 검증 오경보 식별 API API-call constraint checking formal verification false-alarm detection
파일첨부	PDF 다운로드