Formal analysis of policies in wireless sensor network applications
- Resource Type
- Conference
- Authors
- Patrignani, Marco; Matthys, Nelson; Proenca, Jose; Hughes, Danny; Clarke, Dave
- Source
- 2012 Third International Workshop on Software Engineering for Sensor Network Applications (SESENA) Software Engineering for Sensor Network Applications (SESENA), 2012 Third International Workshop on. :15-21 Jun, 2012
- Subject
- Computing and Processing
Communication, Networking and Broadcast Technologies
Components, Circuits, Devices and Systems
Signal Processing and Analysis
Semantics
Cryptography
Wireless sensor networks
Runtime
Prototypes
Syntactics
Model Checking
Formal Methods
Policy-driven Middleware
Wireless Sensor Network Applications
- Language
- ISSN
- 2327-1620
2327-1647
Since wireless sensor network applications are ever growing in scale and complexity, managers require strong formal guarantees that any changes done to the system can be enacted safely. This paper presents the formalisation and analysis of the semantics of policies, tiny software artefacts used to orchestrate wireless sensor network applications. The semantics of policies is formalised in terms of traces augmented with information concerning the constraints under which traces are executed. These traces are composed according to the network topology and subsequently analysed using the mCRL2 model-checking tool. The analysis allows for the detection of semantical inconsistencies that may lead to dangerous or unwanted behaviour of the application based on the policy configuration. An analysis of policies in a real-world system is provided, showing how to verify security and resource usage properties.