A Formal Model for Programming Wireless Sensor Networks

TL;DR

This paper introduces a formal calculus for sensor networks that combines network modeling with device state, providing a foundation for programming languages and runtime systems.

Contribution

It develops a small yet expressive calculus with a type system and invariance results, advancing formal modeling of sensor network programming.

Findings

A new calculus combining network and device state modeling

Type system with invariance guarantees

Framework for programming language development

Abstract

In this paper we present new developments in the expressiveness and in the theory of a Calculus for Sensor Networks (CSN). We combine a network layer of sensor devices with a local object model to describe sensor devices with state. The resulting calculus is quite small and yet very expressive. We also present a type system and a type invariance result for the calculus. These results provide the fundamental framework for the development of programming languages and run-time environments.