Static Analysis by Abstract Interpretation of Functional Properties of Device Drivers in TinyOS
Intervenant(s) : Abdelraouf OUADJAOUT (LIP6)
In this talk, I present a static analysis by Abstract Interpretation for proving the correctness of device drivers in TinyOS. This system is considered as the de facto OS in wireless sensor networks, which are used for monitoring the environment over possibly large geographic areas. The main aim of the analysis is to prove that all possible execution paths follow a correct hardware interaction pattern, that specifies how the driver should access the peripheral in order to activate a specific feature. The proposed analysis is based on a realistic preemptive execution model where interrupts can occur during execution depending on the configuration of the hardware mask registers. I also present some partitioning techniques for tracking crucial information about the system, such as the tasks queue and the hardware state. Finally, I discuss the experimental results that we obtained during the analysis of some real-world device drivers from the current version of TinyOS.
Emmanuel.Chailloux (at) nulllip6.fr