Static Analysis of Device Drivers in TinyOS

Simple item page
dc.contributor.authorOuadjaout, Abdelraouf
dc.contributor.authorLasla, Noureddine
dc.contributor.authorBagaa, Miloud
dc.contributor.authorBadache, Nadjib
dc.date.accessioned2014-02-09T10:26:19Z
dc.date.available2014-02-09T10:26:19Z
dc.date.issued2014-02-05
dc.description.abstractIn 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.fr_FR
dc.identifier.isrnCERIST-DTISI/RR--14-00000006--dz
dc.identifier.urihttp://dl.cerist.dz/handle/CERIST/603
dc.publisherCERIST
dc.relation.ispartofRapports de recherche internes
dc.relation.placeAlger
dc.structureRéseaux de Capteurs et Applicationsfr_FR
dc.subjectStatic analysisfr_FR
dc.subjectDevice driversfr_FR
dc.subjectAbstract Interpretationfr_FR
dc.subjectTinyOSfr_FR
dc.subjectVerificationfr_FR
dc.titleStatic Analysis of Device Drivers in TinyOSfr_FR
dc.typeTechnical Report
Files
Collections
Research Reports