Towards a Model Checker for NesC and Wireless Sensor Networks on 19 Oct 2011

This week we have a new topic from Software Engineering. Manchun will present her work on verifying the correctness of wireless sensor networks applications.

Title: Towards a Model Checker for NesC and Wireless Sensor Networks

Speaker: Manchun Zheng

Description: Wireless sensor networks (WSNs) are expected to run unattendedly for critical tasks. To guarantee the correctness of WSNs is important, but highly nontrivial due to the distributed nature. Traditional tools for debugging and simulating TinyOS are incapable of detecting all possible errors under any circumstance. Bugs occurring during rarely encountered scenarios are difficult (or expensive) to be detected by traditional debugging, testing or simulating. Therefore, there is a need for a technique that is able to automatically search all possible scenarios for potential bugs or errors, in order to ensure the reliability of WSN implementation. Model checking is a technique to verify desirable properties by systematically exploring all possible scenarios of the given system. Model checking has been successfully applied to find intricate errors of both software and hardware systems. However, little has been done to model check WSN implementations. This talk will introduces the domain-specific model checker NesC@PAT that automatically builds models from NesC programs and verifies the programs against various properties. NesC@PAT is the first systematic model checker which tackles errors of WSN implementations at different levels.

See you in SR9, at 4pm!

Leave a Reply

Your email address will not be published. Required fields are marked *