In order to model-check TinyOS embedded sensor applications, we put together a prototype tool chain capable of passing TinyOS code into CBMC, a bounded model checker for ANSI-C (and C++) programs, from the CProver group. Open-source Python, tos2cprover builds on available open-source software 'ply' (a 'lex'/'yacc' Python port) and 'pycparser' (a 'ply' application implementing a parser for standard C).

In the case of, e.g., model-checking TinyOS applications due to run on TelosB sensor nodes (as in the figure below), tos2cprover takes in input the MSP430-specific inlined C program generated by the existing nesc compiler. tos2cprover then models the assembly lines into high-level C, and replaces direct accesses to memory by accesses into a high-level C model of the microcontroller. Then, it instruments the resulting program with calls to interrupt handlers, to mimic the hardware, and minimizes the number of these instrumentations with a partial-order reduction.

The program output by tos2cprover can then be passed to CBMC, which, given an appropriate set of bounds on the program's loops, verifies for standard bugs (e.g. memory violations: out-of-bounds array accesses) and any programmer-added assertions, e.g. assert(_P5OUT & 0x0008) to test that a TelosB led is on.