Skip to Main content Skip to Navigation
Conference papers

Verification of a Failure Management Protocol for Stateful IoT Applications

Umar Ozeer 1 Gwen Salaün 2 Loic Letondeur 1 François-Gaël Ottogalli 1 Jean-Marc Vincent 3
2 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
3 POLARIS - Performance analysis and optimization of LARge Infrastructures and Systems
LIG - Laboratoire d'Informatique de Grenoble, Inria Grenoble - Rhône-Alpes
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, op-timised 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download

https://hal.inria.fr/hal-02930872
Contributor : Gwen Salaün <>
Submitted on : Friday, September 4, 2020 - 3:54:19 PM
Last modification on : Monday, February 15, 2021 - 9:34:02 AM
Long-term archiving on: : Friday, December 4, 2020 - 5:28:49 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

Umar Ozeer, Gwen Salaün, Loic Letondeur, François-Gaël Ottogalli, Jean-Marc Vincent. Verification of a Failure Management Protocol for Stateful IoT Applications. Proc. of FMICS'20, Sep 2020, Vienne, Austria. ⟨10.1007/978-3-030-58298-2_12⟩. ⟨hal-02930872⟩

Share

Metrics

Record views

81

Files downloads

305