Modeling and analyzing wireless sensor networks with VeriSensor: An integrated workflow

Abstract

A Wireless Sensor Network (WSN), made of distributed autonomous nodes, is designed to monitor physical or environmental conditions. WSNs have many application domains such as environment or health monitoring. Their design must consider energy constraints, concurrency issues, node heterogeneity, while still meeting the quality requirements of life-critical applications. Formal verification helps to obtain WSN reliability, but usually requires a high expertise, which limits its adoption in industry. This paper presents VeriSensor, a domain specific modeling language (DSML) for WSNs offering support for formal verification. VeriSensor is designed to be used by WSN experts. It can be automatically translated into a formal specification for model checking. We present the language and its translation into a formal model (we use Instantiable Transition Systems - ITS). A tool has been implemented. We used it to work on a case study, illustrating how several metrics and properties relevant to the domain can be evaluated. © 2013 Springer-Verlag.