Abstract: 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.

Imran Riaz Hasrat, Muhammad Atif and Muhammad Naeem, “Formal Specification and Analysis of Termination Detection by Weight-throwing Protocol” International Journal of Advanced Computer Science and Applications(IJACSA), 9(4), 2018. http://dx.doi.org/10.14569/IJACSA.2018.090441

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