APROV: Another Program Verifier for Embedded Linux Device Drivers

Author

Lee, Oukseh ; Jung, Seung-Cheol ; Ahn, Hyo-Cheon ; Kim, Taeho

Author_Institution

Dept. of CSE, Hanyang Univ., Seoul

Volume

1

fYear

2008

fDate

17-20 Feb. 2008

Firstpage

105

Lastpage

109

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.

Keywords

Linux; application program interfaces; embedded systems; program verification; API; APROV; automatic verification tool; embedded Linux device drivers; error tracking engine; program verifier; shape analysis; Data analysis; Data structures; Debugging; Engines; Error analysis; Error correction; Linux; Shape; Specification languages; Tree data structures; Program verification; backward error-tracing; device driver; shape analysis; static analysis;

fLanguage

English

Publisher

ieee

Conference_Titel

Advanced Communication Technology, 2008. ICACT 2008. 10th International Conference on

Conference_Location

Gangwon-Do

ISSN

1738-9445

Print_ISBN

978-89-5519-136-3

Type

conf

DOI

10.1109/ICACT.2008.4493722

Filename

4493722