Formal specification and verification of reconfigurable wireless sensor networks

This paper deals with reconfigurable wireless sensor networks (to be denoted by RWSN) that should be adapted to their environment under user and energy constraints. RWSN is assumed to be composed of a set of communicating nodes such that each one executes reconfigurable tasks to control local sensors. It is controlled, in a previous research, by a multi-agent architecture. We propose, in this work, timed automata models for the specification and verification of this architecture. Each agent is modeled by timed automaton (TA) to verify functional and temporal constraints when communicating with remote agents. The paper´s contribution is applied to a case study that we simulate and formally verify with UPPAAL environment.