GLONEMO: global and accurate formal models for the analysis of ad-hoc sensor networks

We describe an approach for the formal modeling and analysis of ad-hoc sensor networks, at various levels of abstraction. It is global because it takes into account all the following aspects: a precise modeling of the hardware that implements a single node; the protocol layers; the application code; an abstract model of the physical environment as viewed by the sensors. The global model is executable, to enable validation by simulations, but we also aim at analyzing the global model with various formal validation tools (automatic test, runtime verification techniques, model-checking and abstract interpretations). Each technique or tool may need particular abstractions of the model. In this paper, we illustrate the whole approach with a simple model, and show what formal analysis can be performed on the model.