Parallelising bigraph systems for large-scale wireless sensor networks

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.