My group works to improve the quality of embedded software, for example by:
Also, we are indirectly improving embedded software quality by mechanically finding compiler wrong-code bugs, crash bugs, and missed-optimization bugs. As of February 2011 we've found and reported 325 bugs to various compiler vendors.
Much of our research gets prototyped in the form of tools that are designed to improve the quality of sensor network applications running on TinyOS, and some of these tools are now deployed. For example, starting with TinyOS 2.1, developers can type make micaz safe to create a sensornet image that is dynamically type safe. Starting with the next release after 2.1, users will be able to type make micaz stack-check to statically analyze the sensornet image to detect possible stack overflow errors.
Why embedded software? Because it's hard to get right, it's important to get right, and it's fun to work on. Sometimes my students get to spend the morning working with a theorem prover and the afternoon debugging interrupt handlers with LEDs and a logic analyzer.
See our publications and my CV for more details.