Final published version
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Chapter
Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Chapter
}
TY - CHAP
T1 - On efficient models for model checking message-passing distributed protocols
AU - Bokor, P.
AU - Serafini, M.
AU - Suri, Neeraj
PY - 2010
Y1 - 2010
N2 - The complexity of distributed algorithms, such as state machine replication, motivates the use of formal methods to assist correctness verification. The design of the formal model of an algorithm directly affects the efficiency of the analysis. Therefore, it is desirable that this model does not add "unnecessary" complexity to the analysis. In this paper, we consider a general message-passing (MP) model of distributed algorithms and compare different ways of modeling the message traffic. We prove that the different MP models are equivalent with respect to the common properties of distributed algorithms. Therefore, one can select the model which is best suited for the applied verification technique. We consider MP models which differ regarding whether (1) the event of message delivery can be interleaved with other events and (2) a computation event must consume all messages that have been delivered after the last computation event of the same process. For generalized MP distributed protocols and especially focusing on fault-tolerance, we show that our proposed model (without interleaved delivery events and with relaxed semantics of computation events) is significantly more efficient for explicit state model checking. For example, the model size of the Paxos algorithm is 1/13 th that of existing equivalent MP models. © 2010 Springer-Verlag.
AB - The complexity of distributed algorithms, such as state machine replication, motivates the use of formal methods to assist correctness verification. The design of the formal model of an algorithm directly affects the efficiency of the analysis. Therefore, it is desirable that this model does not add "unnecessary" complexity to the analysis. In this paper, we consider a general message-passing (MP) model of distributed algorithms and compare different ways of modeling the message traffic. We prove that the different MP models are equivalent with respect to the common properties of distributed algorithms. Therefore, one can select the model which is best suited for the applied verification technique. We consider MP models which differ regarding whether (1) the event of message delivery can be interleaved with other events and (2) a computation event must consume all messages that have been delivered after the last computation event of the same process. For generalized MP distributed protocols and especially focusing on fault-tolerance, we show that our proposed model (without interleaved delivery events and with relaxed semantics of computation events) is significantly more efficient for explicit state model checking. For example, the model size of the Paxos algorithm is 1/13 th that of existing equivalent MP models. © 2010 Springer-Verlag.
KW - Common property
KW - Distributed algorithm
KW - Distributed protocols
KW - Explicit-state model checking
KW - Formal model
KW - Message delivery
KW - Message traffic
KW - Model size
KW - Paxos algorithms
KW - Relaxed semantics
KW - State machine replication
KW - Verification techniques
KW - Correctness verifications
KW - Algorithms
KW - Fault tolerance
KW - Formal methods
KW - Mathematical models
KW - Message passing
KW - Quality assurance
KW - Computational complexity
KW - Fault tolerant computer systems
KW - Formal verification
KW - Semantics
KW - Model checking
U2 - 10.1007/978-3-642-13464-7_17
DO - 10.1007/978-3-642-13464-7_17
M3 - Chapter
SN - 3642134637
VL - 6117 LNCS
SP - 216
EP - 223
BT - Formal Techniques for Distributed Systems
PB - Springer
ER -