A Constrained ECA Language Supporting Formal Verification of WSNs

Modern wireless sensor and actuator networks (WSANs) are composed of spatially distributed low cost nodes that can contain different sensors and actuators. Event condition action (ECA) based languages have been widely proposed in order to program WSANs. Implementing applications by using ECA rules is an error-prone process thus various formal methods have been proposed. In spite of this great variety, formal verification of ECA rules has not been tailored to the context of WSANs. In this paper we present IRON, an ECA language for programming WSANs. IRON allows the automatic verifications of ECA rules. These are used by the IRON run-time platform in order to implement the required behaviour