Formal Specification and Analysis of Termination Detection by Weight-throwing Protocol

Termination detection is a critical problem in distributed systems. A distributed computation is called terminated if all of its processes become idle and there are no in-transit messages in communication channels. A distributed termination detection protocol is used to detect the state of a process at any time, i.e., terminated, idle or active. A termination detection protocol on the basis of weight-throwing scheme is described in Yu-Chee Tseng, “Detecting Termination by Weight-throwing in a Faulty Distributed System”, JPDC, 15 February 1995. We apply model checking techniques to verify the protocol and for formal specification and verification the tool-set UPPAAL is used. Our results show that the protocol fails to fulfil some of its functional requirements.

@article{Hasrat2018,
  title     = {Formal Specification and Analysis of Termination Detection by Weight-throwing Protocol},
  journal   = {International Journal of Advanced Computer Science and Applications},
  volume    = {9},
  number    = {4},
  year      = {2018},
  publisher = {The Science and Information Organization},
  author    = {Imran Riaz Hasrat and Muhammad Atif and Muhammad Naeem},
  doi       = {10.14569/IJACSA.2018.090441},
  url       = {https://doi.org/10.14569/IJACSA.2018.090441}
}