Software Analysis for Wireless Sensor Networks

28 pages , UCLA , March 2007.

NESL Technical Report #: TR-UCLA-NESL-200703-07

Traditional static analysis often uses modular checking to verify a subsystem in isolation, while still reasoning about the entire system. Sensor networks, with their physical ties to the environment, are reactive in nature. Unfortunately, many benefits of modular analysis are lost in reactive systems. This loss results from state space pollution caused by reactive events that, from the perspective of the analysis, may fire at any time. My work over the past two years explores a slice of this dilemma. The work resulted in a framework that, when completed within the next two months, will vertically integrate static verification with higher level specifications. This integration allows modular static analysis to proceed with a more limited state space based on assumptions coming from the higher level specification. Load time and run time checks are added to the system to insure that assumptions from the specification are properly followed.

• Roy S Shea

• PDF file of paper
• PDF file of presentation

• Lighthouse : Lighthouse

Report