Formal verification for fault-tolerant architectures: prolegomena to the design of PVS

1995 ◽  
Vol 21 (2) ◽  
pp. 107-125 ◽  
Author(s):  
S. Owre ◽  
J. Rushby ◽  
N. Shankar ◽  
F. von Henke
Keyword(s):  
Formal Verification ◽  
Fault Tolerant

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.

scholarly journals InnoChain: a Distributed Ledger for Industry with Formal Verification on all Implementation Levels

2020 ◽  
Vol 27 (4) ◽  
pp. 454-471
Author(s):  
Vladimir Aleksandrovich Kukharenko ◽  
Kirill Viktorovich Ziborov ◽  
Rafael Faritovich Sadykov ◽  
Alexandr Vladimirovich Naumchev ◽  
Ruslan Maratovich Rezin ◽  
...  
Keyword(s):  
Formal Verification ◽  
Formal Specification ◽  
Fault Tolerant ◽  
Software Implementation ◽  
Actual Behavior ◽  
Consensus Protocol ◽  
Distributed Ledger ◽  
Verification Methods ◽  
Formal Specification And Verification ◽  
Specification And Verification

The extent of formal verification methods applied to 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 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 required to ensure that the software implementation of the DLS nodes complies with this protocol. The verified software implementation of the protocol must run on a fairly reliable operating system. The so-called “smart contracts”, which are an important part of the applied implementations of specific business processes based on DLSs, must be verifiable as well. In this paper, we describe an ongoing industrial project that will result in a DLS verified at least at the four technological levels described above. We then share 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.

Sign in / Sign up

Export Citation Format

Share Document