Ananda Basu, Laurent Mounier, Marc Poulhiès, Jacques Pulou, Joseph Sifakis
Using BIP for Modeling and Verification of Networked Systems -- A Case Study on TinyOS-based Networks (2007)
Using BIP for Modeling and Verification of Networked Systems -- A Case Study on TinyOS-based Networks (2007)
TR-2007-5.pdf
Keywords: Component based modeling, verification, Sensor networks
Abstract: Complex heterogeneous systems such as networked systems, composed of hardware and software, are validated by simulation of physical or virtual prototypes. The main obstacle for the application of verification techniques, which are successfully applied to complex software or hardware, is the lack of methods for building global models faithfully representing their behavior. We apply a model construction methodology using the emph{Behavior-Interaction-Priority} (BIP) component framework, to TinyOS-based networks. The methodology consists in building the model of a node as the composition of a model extracted from a nesC program describing the application, and models of TinyOS components. Models for networks are obtained by composition of models for nodes by using connectors implementing different types of radio channels. This opens the way for enhanced analysis and early error detection by using verification techniques.
