Static Analysis of Device Drivers in TinyOS

Loading...
Thumbnail Image
Date
2014-02-05
Journal Title
Journal ISSN
Volume Title
Publisher
CERIST
Abstract
In this paper, we present SADA, a static analysis tool to verify device drivers for TinyOS applications. Its broad goal is to certify that the execution paths of the application complies with a given hardware specification. SADA can handle a broad spectrum of hardware specifications, ranging from simple assertions about the values of configuration registers, to complex behaviors of possibly several connected hardware components. The hardware specification is expressed in BIP, a language for describing easily complex interacting discrete components. The analysis of the joint behavior of the application and the hardware specification is then performed using the theory of Abstract Interpretation. We have done a set of experiments on some TinyOS applications. Encouraging results are obtained that confirm the effectiveness of our approach.
Description
Keywords
Static analysis, Device drivers, Abstract Interpretation, TinyOS, Verification
Citation
Collections