Formal Specification for Byzantine Fault Tolerant Algorithm Suiting Web Services

A Byzantine Fault Tolerant Algorithm suiting web services is proposed considering the features of web services. There are significant differences between the algorithm and the Castro and Liskov´s well-known practical Byzantine fault tolerance method. First, we have to create replicas on both sides of communicating web services, while in CLBFT´s method, replicas are created only on the server side. Second, due to the autonomous behavior of web services, we have to synchronize the timing of the receiving of messages among replicas. The I/O automata model of the algorithm is presented, and it´s correctness is formally specified and verified.