Using UPPAAL to Verify Recovery in a Fault-tolerant Mechanism Providing Persistent State at the Edge
- Resource Type
- Conference
- Authors
- Bakhshi, Zeinab; Rodriguez-Navas, Guillermo; Hansson, Hans
- Source
- 2021 26th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA ) Emerging Technologies and Factory Automation (ETFA ), 2021 26th IEEE International Conference on. :1-6 Sep, 2021
- Subject
- Communication, Networking and Broadcast Technologies
Components, Circuits, Devices and Systems
Computing and Processing
Robotics and Control Systems
Fault tolerance
Protocols
Conferences
Fault tolerant systems
Containers
Data structures
Data models
- Language
In our previous work we proposed a fault-tolerant persistent storage for container-based fog architecture. We leveraged the use of containerization to provide storage as a containerized application working along with other containers. As a fault-tolerance mechanism we introduced a replicated data structure and to solve consistency issue between the replicas distributed in the cluster of nodes, we used the RAFT consensus protocol. In this paper, we verify our proposed solution using the UPPAAL model checker. We explain how our solution is modeled in UPPAAL and present a formal verification of key properties related to persistent storage and data consistency between nodes.