Using UPPAAL to Verify Recovery in a Fault-tolerant Mechanism Providing Persistent State at the Edge

• 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.

Ämnesord

NATURVETENSKAP  -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Computer Sciences (hsv//eng)

TEKNIK OCH TEKNOLOGIER  -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)

ENGINEERING AND TECHNOLOGY  -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)

Publikations- och innehållstyp

ref (ämneskategori)

kon (ämneskategori)