BROWSE
Detail
Conference Paper
APROV: Another Program Verifier for Embedded Linux Device Drivers
- Authors
- Ouk Seh Lee, Seung-Cheol Jung, Hyo-Cheon Ahn, Tae Ho Kim
- Issue Date
- 2008-02
- Citation
- International Conference on Advanced Communication Technology (ICACT) 2008, pp.105-109
- Language
- English
- Type
- Conference Paper
- Project Code
- 07MW1800, Development of Automatic Code Generation Technology for Device Drivers, Woo Duk Kyun
- Abstract
- 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.
- KSP Keywords
- Automatic Verification, Device driver, Eclipse plug-in, Error tracking, Integrated development environment, Linux driver, Source Code, Verification Tool, abstract interpretation, api usage, embedded linux