Rigorous design of moving sequencer crash tolerant atomic broadcast with unicast broadcast

This article investigates a novel mechanism of atomic broadcast in distributed systems. Various mechanisms are already given for moving sequencer based atomic broadcast like RMP [1], DTP [2] and Pin Wheel [3]. Since all these mechanisms are built on broadcast broadcast (BB) variant [4] of fixed sequencer atomic broadcast hence introduce a very large number of messages [4]. Here we propose a novel mechanism that works on unicast broadcast (UB) invariant of fixed sequencer atomic broadcast in order to build moving sequencer atomic broadcast. The proposed mechanism relies on unicast broadcast hence it will introduce a very less number of messages in comparison to previous mechanisms [4]. Along with broadcast any process may get crash any time. Hence, system must be so efficient such that it can tolerate such crashes and maintains normal behavior so that reliability of system will be maintained. The proposed work will tolerate any crash failure of processes in system and reduce the load on sequencer (by providing an opportunity to each process to be a sequencer). We have used B [5] as formal technique for development of our model. B uses set theory as a modeling notation, refinements to represent system at different abstraction level. We have used Pro B [19] model checker and animator for constraint based checking, discover errors due to invariant violation and deadlocks, thereby, validating the specifications. We present an abstract model specifying atomic broadcast with a fixed sequencer and introducing moving sequencer in first refined version then introduction of crash tolerance in second refined version.