A Constrained ECA Language Supporting Formal Verification of WSNs

Author

Corradini, Flavio ; Culmone, Rosario ; Mostarda, Leonardo ; Tesei, Luca ; Raimondi, Franco

Author_Institution

Comput. Sci. Div., Univ. of Camerino, Camerino, Italy

fYear

2015

fDate

24-27 March 2015

Firstpage

187

Lastpage

192

Abstract

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.

Keywords

actuators; formal verification; programming languages; wireless sensor networks; IRON run-time platform; Integrated Rule ON data; WSAN programming; constrained ECA language; event condition action based languages; formal verification; spatially distributed low cost nodes; wireless sensor and actuator networks; Actuators; Grammar; Heating; Iron; TV; Temperature sensors; Event condition actions; constraints programming; model checking; wireless sensor and actuator networks;

fLanguage

English

Publisher

ieee

Conference_Titel

Advanced Information Networking and Applications Workshops (WAINA), 2015 IEEE 29th International Conference on

Conference_Location

Gwangiu

Print_ISBN

978-1-4799-1774-7

Type

conf

DOI

10.1109/WAINA.2015.109

Filename

7096170