Modular Model-Checking of a Byzantine Fault-Tolerant Protocol
| Autor: | B. F. Jones, Lee Pike |
|---|---|
| Rok vydání: | 2017 |
| Předmět: |
Model checking
Computer science business.industry Node (networking) Distributed computing 020207 software engineering 02 engineering and technology Fault injection Modular design computer.software_genre Code refactoring Scalability 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Fault model business Byzantine fault tolerance computer |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783319572871 NFM |
| DOI: | 10.1007/978-3-319-57288-8_12 |
| Popis: | With proof techniques like IC3 and k-induction, model-checking scales further than ever before. Still, fault-tolerant distributed systems are particularly challenging to model-check given their large state spaces and non-determinism. The typical approach to controlling complexity is to construct ad-hoc abstractions of faults, message-passing, and behaviors. However, these abstractions come at the price of divorcing the model from its implementation and making refactoring difficult. In this work, we present a model for fault-tolerant distributed system verification that combines ideas from the literature including calendar automata, symbolic fault injection, and abstract transition systems, and then use it to model-check various implementations of the Hybrid Oral Messages algorithm that differ in the fault model, timing model, and local node behavior. We show that despite being implementation-level models, the verifications are scalable and modular, insofar as isolated changes to an implementation require isolated changes to the model and proofs. This work is carried out in the SAL model-checker. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|