Experiences with formal specification of fault-tolerant file systems

2008 ◽  
Author(s):  
Roxana Geambasu ◽  
Andrew Birrell ◽  
John MacCormick
Keyword(s):  
Formal Specification ◽  
Fault Tolerant ◽  
File Systems

scholarly journals Verification of HotStuff BFT Consensus Protocol With TLA+/TLC in an Industrial Setting

2021 ◽  
Vol 93 ◽  
pp. 01006
Author(s):  
Vladimir Kukharenko ◽  
Kirill Ziborov ◽  
Rafael Sadykov ◽  
Ruslan Rezin
Keyword(s):  
Formal Verification ◽  
Formal Specification ◽  
Fault Tolerant ◽  
Software Implementation ◽  
Actual Behavior ◽  
Smart Contracts ◽  
Consensus Protocol ◽  
Verification Methods ◽  
Formal Specification And Verification ◽  
Specification And Verification

The extent of formal verification methods applied in industrial projects has always been limited. The proliferation of distributed ledger systems (DLS), also known as blockchain, is rapidly changing the situation. Since the main area of DLSs’ application is the automation of financial transactions, the properties of predictability and reliability are critical for implementing such systems. The actual behavior of the DLS is largely determined by the chosen consensus protocol, which properties require strict specification and formal verification. Formal specification and verification of the consensus protocol is necessary but not sufficient. It is also required to ensure that the software implementation of the DLS nodes complies with this protocol. Finally, the verified software implementation of the protocol must run on a fairly reliable operating system. The financial focus of DLS application has also led to the emergence of the so-called smart contracts, which are an important part of the applied implementations of specific business processes based on DLSs. Therefore, the verifiability of smart contracts is also a critical requirement for industrial DLSs. In this paper, we describe an ongoing industrial project between a large Russian airline and three universities – Innopolis University (IU), Moscow Institute of Physics and Technology (MIPT) and Lomonosov Moscow State University (MSU). The main expected project result is a DLS for more flexible refueling of aircrafts, verified at least at the four technological levels described above. After brief project overview, we focus on our experience with the formal specification and verification of HotStuff, a leader-based fault-tolerant protocol that ensures reaching distributed consensus in the presence of Byzantine processes. The formal specification of the protocol is performed in the TLA+ language and then verified with a specialized TLC tool to verify models based on TLA+ specifications.

XtreemFS

2013 ◽  
pp. 267-285 ◽  
Author(s):  
Jan Stender ◽  
Michael Berlin ◽  
Alexander Reinefeld
Keyword(s):  
Data Storage ◽  
Large Scale ◽  
File System ◽  
Fault Tolerant ◽  
File Systems ◽  
Data Access ◽  
Comprehensive Overview ◽  
Cloud Providers ◽  
The Face ◽  
Cloud Users

Cloud computing poses new challenges to data storage. While cloud providers use shared distributed hardware, which is inherently unreliable and insecure, cloud users expect their data to be safely and securely stored, available at any time, and accessible in the same way as their locally stored data. In this chapter, the authors present XtreemFS, a file system for the cloud. XtreemFS reconciles the need of cloud providers for cheap scale-out storage solutions with that of cloud users for a reliable, secure, and easy data access. The main contributions of the chapter are: a description of the internal architecture of XtreemFS, which presents an approach to build large-scale distributed POSIX-compliant file systems on top of cheap, off-the-shelf hardware; a description of the XtreemFS security infrastructure, which guarantees an isolation of individual users despite shared and insecure storage and network resources; a comprehensive overview of replication mechanisms in XtreemFS, which guarantee consistency, availability, and durability of data in the face of component failures; an overview of the snapshot infrastructure of XtreemFS, which allows to capture and freeze momentary states of the file system in a scalable and fault-tolerant fashion. The authors also compare XtreemFS with existing solutions and argue for its practicability and potential in the cloud storage market.

Fault Tolerant File Models for MPI-IO Parallel File Systems

2007 ◽  
pp. 153-160
Author(s):  
A. Calderón ◽  
F. García-Carballeira ◽  
Florin Isailǎ ◽  
Rainer Keller ◽  
Alexander Schulz
Keyword(s):  
Fault Tolerant ◽  
File Systems ◽  
Parallel File Systems ◽  
Parallel File

Service-Oriented Development of Fault Tolerant Communicating Systems

2010 ◽  
Vol 1 (2) ◽  
pp. 61-85 ◽  
Author(s):  
Linas Laibinis ◽  
Elena Troubitsyna ◽  
Sari Leppänen
Keyword(s):  
Formal Methods ◽  
Formal Specification ◽  
Development Process ◽  
Formal Model ◽  
Fault Tolerant ◽  
Model Driven ◽  
Telecommunication Systems ◽  
Service Oriented ◽  
Model Driven Approach ◽  
High Degree

Telecommunication systems must have a high degree of availability, that is, a high probability of correct and timely provision of requested services. To achieve this, correctness of software for such systems should be ensured. Application of formal methods helps increase confidence in building correct software. However, to be used in practice, formal methods should be well integrated into existing development process. In this paper, the authors propose a formal model-driven approach to development of communicating systems. The authors formalize and extend the Lyra approach—a top-down service-oriented method for development of communicating systems. Lyra is based on transformation and decomposition of models expressed in UML2. The authors formalize Lyra in the B Method by proposing a set of formal specification and refinement patterns reflecting the essential models and transformations of the Lyra phases. Moreover, this paper extends Lyra to integrate reasoning about fault tolerance in the entire development flow.

Sign in / Sign up

Export Citation Format

Share Document