Testa, Alessandro (2013) Dependability Assessment of Wireless Sensor Networks with Formal Methods. [Tesi di dottorato]

[img]
Preview
Documento PDF
alessandro_testa_XXVciclo.pdf

Download (5MB) | Preview
[error in script] [error in script]
Item Type: Tesi di dottorato
Lingua: English
Title: Dependability Assessment of Wireless Sensor Networks with Formal Methods
Creators:
CreatorsEmail
Testa, Alessandroa.testa@unina.it
Date: 30 March 2013
Number of Pages: 169
Institution: Università degli Studi di Napoli Federico II
Department: Ingegneria Elettrica e delle Tecnologie dell'Informazione
Scuola di dottorato: Ingegneria dell'informazione
Dottorato: Ingegneria informatica ed automatica
Ciclo di dottorato: 25
Coordinatore del Corso di dottorato:
nomeemail
Garofalo, Francescofrancesco.garofalo@unina.it
Tutor:
nomeemail
Cinque, Marcellomacinque@unina.it
Coronato, Antonioantonio.coronato@na.icar.cnr.it
Date: 30 March 2013
Number of Pages: 169
Uncontrolled Keywords: Dependability, WSN, Verification
Settori scientifico-disciplinari del MIUR: Area 09 - Ingegneria industriale e dell'informazione > ING-INF/05 - Sistemi di elaborazione delle informazioni
Date Deposited: 05 Apr 2013 12:10
Last Modified: 22 Jul 2014 12:36
URI: http://www.fedoa.unina.it/id/eprint/9106
DOI: 10.6092/UNINA/FEDOA/9106

Abstract

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.

Actions (login required)

View Item View Item