Embedded network systems support a variety of application domains, including environmental monitoring, social networking, and healthcare. These large networks of low-powered microcontroller-based nodes present challenges in ensuring correctness of the software that runs on these systems. Most embedded networked systems are programmed in C. Verifying software written in C is difficult. In this paper, we take a different approach: We report on our work using the RESOLVE language to program embedded networked systems. Our compiler leverages the RESOLVE verification system and maintains the correctness guarantees established during verification. The verified code is then translated into property-preserving C code that can run on the target hardware.
展开▼
