A refined sensor-ability: Applying process algebra to sensor network analysis

Allan McInnes

Communicating Sequential Processes (CSP): mutually consistent denotationally; operationally; and algebraic semantics.

Refinement can provide verification.

Node modeling. Example node:

• TinyOS: programmed in nesC; component-based; Event driven.

• TinyOS concurrency: Interrupts (asynchronous) and Task scheduling (synchronous). Task scheduling done with a FIFO queue.
• Model executed on FDR2.

Network modeling:

• Time Flooding Synchronization protocol: same time base (only says all nodes will have the same time, whatever it is).
• Model maxed out at seven nodes.

Further refinements:

• Network level models against node models. High -> Low level.
• Check fault tolerance in a network.