차량전장용 소프트웨어의 API 제약사항 위배여부 탐지를 위한 실행경로 탐색방법과 모델검증 방법의 비교

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

연구문헌

국내 논문지

홈 > 연구문헌 > 국내 논문지 > 한국정보처리학회 논문지 > 정보처리학회 논문지 소프트웨어 및 데이터 공학

정보처리학회 논문지 소프트웨어 및 데이터 공학

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

한글제목(Korean Title)	차량전장용 소프트웨어의 API 제약사항 위배여부 탐지를 위한 실행경로 탐색방법과 모델검증 방법의 비교
영문제목(English Title)	Comparison of Path Exploration and Model Checking Techniques for Checking Automotive API Call Safety
저자(Author)	김동우 최윤자 Dongwoo Kim Yunja Choi
원문수록처(Citation)	VOL 05 NO. 12 PP. 0615 ~ 0622 (2016. 12)
한글내용 (Korean Abstract)	차량전장용 제어 소프트웨어는 표준에 명시된 시스템 호출 제약사항을 위배할 경우 심각한 안전성 위협을 초래할 수 있다. 그러나 제약사항 위배는 실행경로가 복잡해질 경우 수동분석으로 색출하기 어렵고 테스팅을 통해 찾아내기도 어려워 이에 특화된 검증 방법이 필요하다. 본 연구에서는 차량전장용 제어 소프트웨어의 시스템 호출 제약사항 위배 여부를 효과적으로 검증하기 위한 두 가지 방법을 소개하고 그 효과를 실험적으로 비교하였다. 첫 번째 방법은 애플리케이션의 모든 가능한 실행경로를 탐색하고 각 경로의 제약사항 준수여부를 확인하는 방법이며, 두 번째 방법은 모델 검증 도구를 이용하여 애플리케이션이 오토마타로 표현된 제약사항을 위배하는 경우가 발생가능한지 확인하는 방법이다. 각 방법을 구현하고 실험한 결과 실행경로를 이용한 방법은 오탐을 유발하고 몇 가지 제약사항 위반을 놓치는 경우가 있는데 반해서 모델 검증을 이용한 방법은 오탐이 없었으며 비교적 큰 애플리케이션을 대상으로 보다 빠른 시간 내에 검증을 수행할 수 있음을 보였다.
영문내용 (English Abstract)	Automotive control software can be a source of critical safety issues when developers do not comply system constraints. However, a violation is difficult to identify in complicated source code if not supported by an automated verification tool. This paper introduces two possible approaches that check whether an automotive control software complies API call constraints to compare their performance and effectiveness. One method statically analyzes the source code and explores all possible execution paths, and the other utilizes a model checker to monitor constraint violations for a given set of constraint automata. We have implemented both approaches and performed a series of experiments showing that the approach with model-checking finds constraint violations more accurately and scales better.
키워드(Keyword)	차량전장소프트웨어 애플리케이션 프로그래밍 인터페이스 OSEK/VDX 제약사항 패턴 정적분석 모델검증 Automotive Software API OSEK/VDX Constraint Pattern Static Analysis Model Checking
파일첨부	PDF 다운로드