Verification of a Failure Management Protocol for Stateful IoT Applications

Abstract

Fog computing provides computing, storage and communication resources at the edge of the network, near the physical world. Devices deployed in the Fog have interesting properties such as short delays, responsiveness, optimised communications and privacy. However, these devices have low stability and are prone to failures. Thus, there is a need for management protocols to tolerate failures of IoT applications in the Fog. We propose a failure management protocol which recovers from failures of devices and software elements involved in an IoT application. Designing such highly distributed management protocols is a difficult and error-prone task. Therefore, the main contribution of this paper is the formal specification and verification of this failure management protocol. Formal specification is achieved using a process algebraic language. The corresponding formal model was used to carry out extensive analysis of the protocol to ensure that it preserves important architectural invariants and functional properties. The verification step was performed using model checking techniques. The analysis of the protocol was a success because it allowed us to detect and correct several issues in the protocol.