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.