Power Analysis of Interrupt-Driven and Multi-Threaded Programs ∗

1 Abstract We aim to combine software verification techniques to achieve static power analysis for interrupt-driven and multi-threaded programs, which are used in many networked embedded systems. The goal is achieved by 1) control flow analysis, 2) instruction-level power estimation/emulation, 3) thread-context model, and 4) counterexample guided refinement. One essential requirement for sensor networks is the reliability of applications since sensors are planned to deploy into the area once and unattended for a period of time without maintenance. An interesting focus is the lifetime of the sensor network. In some sense, the lifetime for a hardware configuration reflects the period from the beginning till it out of charge. Hence, how to achieve precise power analysis attracts more and more research attention. Previous researchers focus on simulation/emulation, in which they calculate the power consumption of their implementation along some specified execution. Since concurrent interactions between components may make the behavior of applications hard to predict, it appears to be attractive to adopt formal verification to support power analysis. The hurdle relies on handling the interaction between concurrent tasks and hardware interrupt, which raise exponential behaviors of the system and makes dynamic methods, e.g., testing/simulation [17, 23], run out of ability. While symbolic model checking shows some promise, previous works focused on explicit problems of programming languages, such as data race checking [14], and none of them address the power analysis, an emerging requirement for sensor networks. To address this issue, we aim to extend symbolic model checking to power analysis of multi-threaded programs, such that most networked embedded systems, e.g., nesC/tinyOS and SOS applications, can be analyzed with guarantee. The extension is achieved by combining the following techniques: 1)control flow analysis [19] 2)