Graphical Animations of the Suzuki-Kasami Distributed Mutual Exclusion Protocol
Dang Duy Bui, Kazuhiro Ogata · Proceedings · 2019
A state machine that formalizes a distributed mutual exclusion protocol called the Suzuki-Kasami protocol is graphically animated.The network with which messages are exchanged among nodes in the protocol is displayed as follows: some limited number of messages in the network are displayed and the others are depressed when there are many messages in the network.We prepare one place dedicated to the message that has been just put into the network by a node (or just sent by a node) and one place dedicated to the message that has been just received by a node (just deleted from the network by a node).The main purpose of graphically animating state machines is to make it possible for humans to perceive characteristics or properties of the state machines by observing their graphical animations.We can guess some properties of the state machine formalizing the Suzuki-Kasami protocol by observing graphical animations of the state machine and confirm them by model checking, which demonstrates that state machine graphical animations could make humans perceive state machine properties.