Formal Specification for Byzantine Fault Tolerant Algorithm Suiting Web Services

Author

Zhou, Wei ; Chen, Liu

Author_Institution

Comput. Sch., Wuhan Univ., Wuhan, China

fYear

2011

fDate

22-23 Oct. 2011

Firstpage

35

Lastpage

38

Abstract

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.

Keywords

Web services; automata theory; formal specification; software fault tolerance; Byzantine fault tolerant algorithm suiting Web services; CLBFT method; I/O automata model; formal specification; Automata; Fault tolerance; Fault tolerant systems; Protocols; Security; Web services; Byzantine fault; I/O automata; replica; web service;

fLanguage

English

Publisher

ieee

Conference_Titel

Intelligence Information Processing and Trusted Computing (IPTC), 2011 2nd International Symposium on

Conference_Location

Hubei

Print_ISBN

978-1-4577-1130-5

Type

conf

DOI

10.1109/IPTC.2011.16

Filename

6103530