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 [2020-....] - Construction of verified concurrent systems [2020-....]
Inria Grenoble - Rhône-Alpes, LIG [2020-....] - Laboratoire d'Informatique de Grenoble [2020-....]
3 POLARIS [2020-....] - Performance analysis and optimization of LARge Infrastructures and Systems [2020-....]
Inria Grenoble - Rhône-Alpes, LIG [2020-....] - Laboratoire d'Informatique de Grenoble [2020-....]
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 metadatas

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 : Saturday, September 5, 2020 - 3:32:40 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02930872, version 1

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. ⟨hal-02930872⟩

Share

Metrics

Record views

44

Files downloads

44