Search

While the increasing ubiquity of embedded devices has given rise to the 'smart' moniker applied to everyday objects, the underpinning wireless communication protocols collectively incorporate them into the Internet of Things (IoT). These protocols facilitate communication to, from, and between objects, and have spawned ever more sophisticated applications in both the home and in industry. While much of the publicity around this phenomenon has focused on domestic uses, a quiet revolution has been taking place within industrial and commercial sectors: as the initial promises of IoT are finally met by technological capability. It is here, in the Industrial Internet of Things (IIoT), where there is the opportunity to streamline operations, such as managing warehouse stock for Just-in-Time (JIT) manufacturing; support safety-critical systems through the complex monitoring of sensor and actuator networks; and offer new business models, where IoT infrastructure can be offered as a service (IoTaaS). Traditionally, low-power wireless mesh networks have been at the forefront of the IoT conversation. However, the increasing complexity of these networks has laid bare the shortcomings inherent in current control architectures and protocols, where lossy channels and multi-hop topologies present significant challenges. To address these issues, there has been considerable interest in applying the concepts of Software Defined Networking (SDN), which over the past decade has liberated data centre and campus network management from reliance on vertical infrastructure practices. However, the centralised SDN approach faces considerable challenges in the constrained environments present in low-power wireless networks. This thesis explores not only how SDN concepts can be used to provide dynamic and flexible control in IIoT, but crucially how to address and manage the SDN overhead. It presents analytical, simulated, and experimental results, as well as the design and implementation of two novel SDN architectures for low-power wireless networks: μSDN and Atomic-SDN. These results demonstrate both that the challenges of applying SDN within constrained IoT networks can be overcome, and that SDN can be used to address the complex and diverse traffic requirements of IIoT applications across low-power wireless networks. The synchronous flooding approach of Atomic-SDN, in particular, provides an effective means of achieving the one-to-many traffic pattern required in distributed control systems, and makes it a highly promising solution for deploying SDN within low-power wireless IIoT networks.

In software engineering, formal methods are mathematical-based techniques that are used in the specification, development and verification of algorithms and programs in order to provide reliability and robustness of systems. One of the most difficult challenges for software engineering is to tackle the complexity of algorithms and software found in concurrent systems. Networked systems have come to prominence in many aspects of modern life, and therefore software engineering techniques for treating concurrency in such systems has acquired a particular importance. Algorithms in the software of concurrent systems are used to accomplish certain tasks which need to comply with the properties required of the system as a whole. These properties can be broadly subdivided into `safety properties', where the requirement is `nothing bad will happen', and `liveness properties', where the requirement is that `something good will happen'. As such, specifying network algorithms and their safety and liveness properties through formal methods is the aim of the research presented in this thesis. Since temporal logic has proved to be a successful technique in formal methods, which have various practical applications due to the availability of powerful model-checking tools such as the NuSMV model checker, we will investigate the specification and verification of network algorithms using temporal logic and model checking. In the first part of the thesis, we specify and verify safety properties for network algorithms. We will use temporal logic to prove the safety property of data consistency or serializability for a model of the execution of an unbounded number of concurrent transactions over time, which could represent software schedulers for an unknown number of transactions being present in a network. In the second part of the thesis, we will specify and verify the liveness properties of networked flooding algorithms. Considering the above in more detail, the first part of this thesis specifies a model of the execution of an unbounded number of concurrent transactions over time in propositional Linear Temporal Logic (LTL) in order to prove serializability. This is made possible by assuming that data items are ordered and that the transactions accessing these data items respects this order, as then there is a bound on the number of transactions that need to be considered to prove serializability. In particular, we make use of recent work which places such bounds on the number of transactions needed when data items are accessed in order, but do not have to be accessed contiguously, i.e., there may be `gaps' in the data items being accessed by individual transactions. Our aim is to specify the concurrent modification of data held on routers in a network as a transactional model. The correctness of the routing protocol and ensuring safety and reliability then corresponds to the serializability of the transactions. We specify an example of routing in a network and the corresponding serializability condition in LTL. This is then coded up in the NuSMV model checker and proofs are performed. The novelty of this part is that no previous research has used a method for detecting serializablity and cycles for unlimited number of transactions accessing the data on routers where the transactions way of accessing the data items on the routers have a gap. In addition to this, linear temporal logic has not been used in this scenario to prove correctness of the network system. This part is very helpful in network administrative protocols where it is critical to maintain correctness of the system. This safety property can be maintained using the presented work where detection of cycles in transactions accessing the data items can be detected by only checking a limited number of cycles rather than checking all possible cycles that can be caused by the network transactions. The second part of the thesis offers two contributions. Firstly, we specify the basic synchronous network flooding algorithm, for any fixed size of network, in LTL. The specification can be customized to any single network topology or class of topologies. A specification for the termination problem is formulated and used to compare different topologies with regards to earlier termination. We give a worked example of one topology resulting in earlier termination than another, for which we perform a formal verification using the NuSMV model checker. The novelty of the second part comes in using linear temporal logic and the NuSMV model checker to specify and verify the liveness property of the flooding algorithm. The presented work shows a very difficult scenario where the network nodes are memoryless. This makes detecting the termination of network flooding very complicated especially with networks of complex topologies. In the literature, researchers focussed on using testing and simulations to detect flooding termination. In this work, we used a robust technique and a rigorous method to specify and verify the synchronous flooding algorithm and its termination. We also showed that we can use linear temporal logic and the model checker NuSMV to compare synchronous flooding termination between topologies. Adding to the novelty of the second contribution, in addition to the synchronous form of the network flooding algorithm, we further provide a formal model of bounded asynchronous network flooding by extending the synchronous flooding model to allow a sent message, non-deterministically, to either be received instantaneously, or enter a transit phase prior to being received. A generalization of `rounds' from synchronous flooding to the asynchronous case is used as a unit of time to provide a measure of time to termination, as the number of rounds taken, for a run of an asynchronous system. The model is encoded into temporal logic and a proof obligation is given for comparing the termination times of asynchronous and synchronous systems. Worked examples are formally verified using the NuSMV model checker. This work offers a constraint-based methodology for the verification of liveness properties of software algorithms distributed across the nodes in a network.