Formal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT Systems
Formal Verification of Synchronisation, Gossip and Environmental Effects for Critical IoT Systems
复制标题
关键物联网系统同步、八卦和环境影响的正式验证
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
J. Mccann
中科院分区：
文献类型：
--
作者：
M. Webster;Michael J. Breza;C. Dixon;Michael Fisher;J. Mccann
物联网（IoT）有望在监测和控制各种应用方面带来革命，从城市供水网络和精准农业食品生产，到车辆连接和医疗保健监测。对于这些关键领域的应用，物联网系统的控制软件和协议必须经过验证，既强大又可靠。物联网系统鲁棒性和可靠性的两个最大障碍是环境条件对硬件的影响，以及协议使用的参数选择。在本文中，我们使用概率模型检查来验证无线传感器网络（WSNs）的同步和传播协议是正确的，其要求，并没有受到不利影响的环境。我们将展示如何将协议转换为逻辑模型，然后使用概率模型检查器PRISM进行分析。使用这种方法，我们证明了在何种情况下，该协议是保证同步的所有节点和传播新的信息到所有节点。我们还研究了同步的界限，因为环境改变了硬件时钟的性能，并调查这种方法的可扩展性约束。
The Internet of Things (IoT) promises a revolution in the monitoring and control of a wide range of applications, from urban water supply networks and precision agriculture food production, to vehicle connectivity and healthcare monitoring. For applications in such critical areas, control software and protocols for IoT systems must be verified to be both robust and reliable. Two of the largest obstacles to robustness and reliability in IoT systems are effects on the hardware caused by environmental conditions, and the choice of parameters used by the protocol. In this paper we use probabilistic model checking to verify that a synchronisation and dissemination protocol for Wireless Sensor Networks (WSNs) is correct with respect to its requirements, and is not adversely affected by the environment. We show how the protocol can be converted into a logical model and then analysed using the probabilistic model-checker, PRISM. Using this approach we prove under which circumstances the protocol is guaranteed to synchronise all nodes and disseminate new information to all nodes. We also examine the bounds on synchronisation as the environment changes the performance of the hardware clock, and investigate the scalability constraints of this approach.