Parallelising bigraph systems for large-scale wireless sensor networks

物联网(IoT)正在成为我们日常生活中不可或缺的一部分。使用无线传感器网络(WSN)技术，物联网系统可以提供各种服务，从家庭中的“智能”设备和家用电器，到城市范围或国际规模的交通和电力系统。这些系统的广泛采用在很大程度上取决于它们的可靠性、安全性、安全性和弹性，特别是在人类处于循环中的情况下。然而，当前的工程实践不能保证在物联网系统运行时始终满足这些特性。其结果是，在这些系统的设计阶段，潜在的问题仍然是无法预见的，只是在部署后才会出现，可能会产生悲惨的后果。现实世界的物联网部署可能通常由数千个不同种类的传感器、执行器和连接组成，这一事实进一步加剧了这一点。长期以来，人们一直认为，正规的建模和分析对于实现严格的系统工程、提供可靠性、安全性和性能保证非常重要。尽管正式模型最常用于在实现之前检查系统设计，但它们也可以在运行时用于检查已经部署的系统的需求。最近的工作提出了基于二元图的方法，这是一种对在空间、时间、连通性和交互作用中演变的系统进行通用建模的形式主义。系统的时间演化由重写规则指定，属性由双图和时间通道结构上的模式表示。虽然这些技术中的一些可以很容易地应用于物联网系统的建模和分析，但需要进行更多的研究才能将双图扩展到大规模系统。

The Internet of Things (IoT) is becoming an integral part of our everyday lives. Using Wireless Sensor Network (WSN) technologies, IoT systems can provide a variety of services that range from "smart" devices and appliances in the home to traffic and power systems on a city-wide, or international scale. The widespread adoption of these systems is critically dependent on them being reliable, safe, secure, and resilient, especially when humans are in the loop. However, current engineering practice cannot provide guarantees that these properties are always met when an IoT system is operating. The consequence is that potential issues remain unforeseen during the design phase of these systems only to later emerge after deployment, potentially with tragic consequences. This is further exacerbated by the fact that real-world IoT deployments may often consist of thousands of heterogeneous sensors, actuators, and connections.Formal modelling and analysis have long been recognised as important to enabling rigorous systems engineering, delivering assurances of reliability, security and performance. Although formal models are most commonly used to check system designs ahead of implementation, they may also be used at run time to check the requirements of a system that has already been deployed. Recent works have proposed approaches based on bigraphs, a universal modelling formalism for systems that evolve in space, time, connectivity and interaction. The temporal evolution of a system is specified by rewrite rules and properties are expressed by patterns over the structure of bigraphs and temporal modalities. Although some of these techniques can be readily applied to model and analyse IoT systems, more research is needed to scale bigraphs to large-scale systems.