Thursday, September 24, 2009

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.

No comments: