CodeAnt : 소프트웨어 검증 효율 향상을 위한 코드 슬라이싱 도구

박민규; 김동우; 최윤자; Mingyu Park; Dongwoo Kim; Yunja Choi

연구문헌

국내 논문지

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

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

Current Result Document : 6 / 6 이전건

한글제목(Korean Title)	CodeAnt : 소프트웨어 검증 효율 향상을 위한 코드 슬라이싱 도구
영문제목(English Title)	CodeAnt : Code Slicing Tool for Effective Software Verification
저자(Author)	박민규 김동우 최윤자 Mingyu Park Dongwoo Kim Yunja Choi
원문수록처(Citation)	VOL 04 NO. 01 PP. 0001 ~ 0008 (2015. 01)
한글내용 (Korean Abstract)	고안전성이 요구되는 소프트웨어의 경우 극히 낮은 확률로 발생하는 오류로 인하여 전체시스템의 안전에 치명적인 상황을 야기할 수 있으므로, 철저한 안전성 검증이 요구된다. 하지만 모든 가능한 실행경로를 고려해야 하는 안전성 검증은 고비용이 발생한다는 단점이 있다. 본 논문에서는 안전성 검증의 고비용 문제를 개선하기 위해 안전성 특질을 기준으로 코드 슬라이싱 기법[1]을 구현한 도구를 개발하였다. 개발한 도구를 OSEK/VDX[2] 기반의 개방형 차량 전장용 운영체제인 Trampoline[3] 소스코드에 적용한 결과 분석 대상의 코드의 크기를 평균 71% 줄일 수 있었고, 실제 검증을 수행했을 시에도 도구 적용 이전보다 검증 비용을 절감할 수 있었음을 보였다.
영문내용 (English Abstract)	Safety critical systems require exhaustive verification of safety properties, because even a single corner-case fault can cause a critical safety failure. However, existing verification approaches are too costly in terms of time and computational resource required, making it hard to be applied in practice. In this paper, we implemented a tool for minimizing the size of the verification target w.r.t. verification properties to check, based on program slicing technique[1]. The efficacy of program slicing using our tool is demonstrated in a case study with a verification target Trampoline[3], which is an open source automotive operating system compliant with OSEK/VDX[2]. Experiments have shown enhanced performance in verification, with a 71% reduction in the size of the code.
키워드(Keyword)	코드 슬라이싱 안전성 검증 차량 전장용 운영체제
파일첨부	PDF 다운로드