A Formal Methodology to Design and Deploy Dependable Wireless Sensor NetworksReportar como inadecuado


A Formal Methodology to Design and Deploy Dependable Wireless Sensor Networks


A Formal Methodology to Design and Deploy Dependable Wireless Sensor Networks - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1

Ministero dell’Economia e delle Finanze, Rome 00187, Italy

2

Dipartimento di Ingegneria Elettrica e delle Tecnologie dell’Informazione, University of Naples -Federico II-, Naples 80125, Italy

3

CNR-ICAR, Naples 80131, Italy

4

Department of Computer Science and R.G. on Development of Intelligent Environments, Middlesex University of London, London NW4 2SH, UK





*

Author to whom correspondence should be addressed.



Academic Editor: Leonhard M. Reindl

Abstract Wireless Sensor Networks WSNs are being increasingly adopted in critical applications, where verifying the correct operation of sensor nodes is a major concern. Undesired events may undermine the mission of the WSNs. Hence, their effects need to be properly assessed before deployment, to obtain a good level of expected performance; and during the operation, in order to avoid dangerous unexpected results. In this paper, we propose a methodology that aims at assessing and improving the dependability level of WSNs by means of an event-based formal verification technique. The methodology includes a process to guide designers towards the realization of a dependable WSN and a tool -ADVISES- to simplify its adoption. The tool is applicable to homogeneous WSNs with static routing topologies. It allows the automatic generation of formal specifications used to check correctness properties and evaluate dependability metrics at design time and at runtime for WSNs where an acceptable percentage of faults can be defined. During the runtime, we can check the behavior of the WSN accordingly to the results obtained at design time and we can detect sudden and unexpected failures, in order to trigger recovery procedures. The effectiveness of the methodology is shown in the context of two case studies, as proof-of-concept, aiming to illustrate how the tool is helpful to drive design choices and to check the correctness properties of the WSN at runtime. Although the method scales up to very large WSNs, the applicability of the methodology may be compromised by the state space explosion of the reasoning model, which must be faced by partitioning large topologies into sub-topologies. View Full-Text

Keywords: Wireless Sensor Networks; formal methods; dependability; metrics; modeling Wireless Sensor Networks; formal methods; dependability; metrics; modeling





Autor: Alessandro Testa 1, Marcello Cinque 2, Antonio Coronato 3,* and Juan Carlos Augusto 4

Fuente: http://mdpi.com/



DESCARGAR PDF




Documentos relacionados