[Home]

Software Verification for TinyOS

Links and Documentation

Under the EPSRC UbiVal project, we developed prototype tools for software verification (i.e. model checking directly from source code) for TinyOS sensor applications, on two subtopics:

1. verification for MSP430-specific embedded C code generated by the nesc compiler:
   1. UbiVal project report [pdf]
   2. IPSN '10 Poster Abstract: Software Verification for TinyOS [pdf]
   3. The Tos2CProver repository at Google Code
2. verification for programmer applications written in the C TOSThreads API:
   1. AmI '09 Bug-Free Sensors: The Automatic Verification of Context-Aware TinyOS Applications [pdf]

Summary

Microcontroller-specific software such as the one generated by the nesc TinyOS compiler is a low-level flavour of C with assembly snippets and direct access to memory, as the memory is mapped by the microcontroller.

In order to apply software verification to such sensor code, we built 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. Our tool, tos2cprover, "links" the nesc compiler and CBMC (as in the figure). It takes in input the MSP430-specific inlined C program generated by the 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 existence of hardware interrupts.

The microcontroller's model replaces hardware registers with C variables, e.g., unsigned short _R2; for the Status Register, and unsigned char _P5OUT; for the output register of Peripheral Port 5 (where TelosB wires the three leds, as in the MSP430's pin map to the right). As the peripherals are memory-mapped by the MCU (such as MSP430's memory map below; e.g., the output register of port 5 is mapped at address 0x0031). Then, any direct access at 0x0031, such as the line

*(uint8_t*)49U &= ~(0x01 << 6);

_P5OUT &= ~(0x01 << 6);

Calls to interrupt handlers:

   /* IRQ INSTRUMENTATION */
    if (int_enabled()) { 
        disable_int(); 
        sig_ADC_VECTOR(); 
        enable_int();
    }