Testa Alessandro, Cinque Marcello, Coronato Antonio, Augusto Juan Carlos
Ministero dell'Economia e delle Finanze, Rome 00187, Italy.
Dipartimento di Ingegneria Elettrica e delle Tecnologie dell'Informazione, University of Naples "Federico II", Naples 80125, Italy.
Sensors (Basel). 2016 Dec 23;17(1):19. doi: 10.3390/s17010019.
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.
无线传感器网络（WSNs）越来越多地应用于关键应用中，在这些应用中，验证传感器节点的正确运行是一个主要问题。不良事件可能会破坏无线传感器网络的任务。因此，在部署之前需要对其影响进行适当评估，以获得良好的预期性能水平；在运行期间，也要进行评估，以避免出现危险的意外结果。在本文中，我们提出了一种方法，旨在通过基于事件的形式化验证技术来评估和提高无线传感器网络的可靠性水平。该方法包括一个指导设计人员实现可靠无线传感器网络的过程，以及一个简化其应用的工具（“ADVISES”）。该工具适用于具有静态路由拓扑的同构无线传感器网络。它允许自动生成形式化规范，用于在设计时和运行时检查正确性属性并评估可靠性指标，适用于可以定义可接受故障百分比的无线传感器网络。在运行时，我们可以根据设计时获得的结果检查无线传感器网络的行为，并检测突然和意外的故障，以便触发恢复程序。在两个案例研究的背景下展示了该方法的有效性，作为概念验证，旨在说明该工具如何有助于推动设计选择并在运行时检查无线传感器网络的正确性属性。尽管该方法可以扩展到非常大的无线传感器网络，但该方法的适用性可能会受到推理模型状态空间爆炸的影响，必须通过将大型拓扑划分为子拓扑来解决这一问题。
