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

[img]
Anteprima
Documento PDF
alessandro_testa_XXVciclo.pdf

Download (5MB) | Anteprima
[error in script] [error in script]
Tipologia del documento: Tesi di dottorato
Lingua: English
Titolo: Dependability Assessment of Wireless Sensor Networks with Formal Methods
Autori:
AutoreEmail
Testa, Alessandroa.testa@unina.it
Data: 30 Marzo 2013
Numero di pagine: 169
Istituzione: Università degli Studi di Napoli Federico II
Dipartimento: 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
Data: 30 Marzo 2013
Numero di pagine: 169
Parole chiave: Dependability, WSN, Verification
Settori scientifico-disciplinari del MIUR: Area 09 - Ingegneria industriale e dell'informazione > ING-INF/05 - Sistemi di elaborazione delle informazioni
Depositato il: 05 Apr 2013 12:10
Ultima modifica: 22 Lug 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.

Downloads

Downloads per month over past year

Actions (login required)

Modifica documento Modifica documento