ETRI-Knowledge Sharing Plaform

ENGLISH

성과물

논문 검색
구분 SCI
연도 ~ 키워드

상세정보

학술대회 APROV: Another Program Verifier for Embedded Linux Device Drivers
Cited 0 time in scopus Download 1 time Share share facebook twitter linkedin kakaostory
저자
이욱세, 정승철, 안효천, 김태호
발행일
200802
출처
International Conference on Advanced Communication Technology (ICACT) 2008, pp.105-109
DOI
https://dx.doi.org/10.1109/ICACT.2008.4493722
협약과제
07MW1800, 디바이스 드라이버 소스 코드 자동 생성 기술개발, 우덕균
초록
We devise an automatic verification tool for embedded Linux driver source code. Our tool can verify whether a device driver is correctly implemented without violating API usage rules, causing pointer errors, and leaking memory. The verification engine uses a lightweight version of shape analysis and an abstract interpretation on integer values. For debugging errors which the verifier finds out, we devise an error tracking engine which accurately points out the possible sources of errors. Our verifier and error tracer are embedded into our integrated development environment for embedded Linux device drivers as an eclipse plug-in.
키워드
Backward error-tracing, Device driver, Program verification, Shape analysis, Static analysis
KSP 제안 키워드
Automatic Verification, Backward error, Device driver, Eclipse plug-in, Error tracking, Integrated development environment, Linux driver, Source Code, Verification Tool, abstract interpretation, api usage