Dependability Assessment of Wireless Sensor Networks with Formal Methods

Wireless Sensor Networks (WSNs) are increasingly being adopted in critical applications, where verifying the correct operation of sensor nodes is a major concern. Undesired events, such as node crash and packet loss, may undermine the dependability of the WSN. Hence their effects need to be properly assessed from the early stages of the development process onwards to minimize the chances of unexpected problems during use. It is also necessary to monitor the system during operation in order to avoid unexpected results or dangerous effects. In this thesis we propose a framework to investigate the correctness of the design of a WSN from the point of view of its dependability, i.e., resilience to undesired events. The framework is based on the Event Calculus formalism and it is backed-up by a support tool aimed to simplify its adoption by system designers. The tool allows to specify the target WSN in a user-friendly way and it is able to generate automatically the Event Calculus specifications used to check correctness properties and evaluate dependability metrics, such as connection resiliency, coverage and lifetime. It is able to work at design time and runtime. In particular at runtime the tool works a server that is in waiting for new events coming from the WSN and, performed the reasoning using the same specifications, is able to do prediction about future criticalities of the WSN. The effectiveness of the approach is shown in the context of five case studies, aiming to illustrate how the framework is helpful to drive design choices by means of what-if scenario analysis and robustness checking, and to check the correctness properties of the WSN at runtime.