Sökning: WFRF:(Rodriguez Navas Guillermo) >
Using UPPAAL to Ver...
Using UPPAAL to Verify Recovery in a Fault-tolerant Mechanism Providing Persistent State at the Edge
-
- Bakhshi Valojerdi, Zeinab, 1986- (författare)
- Mälardalens högskola,Inbyggda system
-
- Rodriguez-Navas, Guillermo (författare)
- Mälardalens högskola,Inbyggda system
-
- Hansson, Hans (författare)
- Mälardalens högskola,Inbyggda system
-
(creator_code:org_t)
- Västerås : Institute of Electrical and Electronics Engineers (IEEE), 2021
- 2021
- Engelska.
-
Ingår i: 26th IEEE International Conference on Emerging Technologies and Factory Automation, ETFA 2021. - Västerås : Institute of Electrical and Electronics Engineers (IEEE). - 9781728129891
- Relaterad länk:
-
https://doi.org/10.1...
-
visa fler...
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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)
Hitta via bibliotek
Till lärosätets databas