Abstract—Abstract—Probabilistic model checking is used for verifying stochastic behaviors of systems. Model checking plays imperative role for scrutinizing of novel protocols in almost every field including computer communications, networks, security, and biology prior to extensive simulations. In this paper we present an overview of few diverse case studies which are implemented using one of the leading probabilistic symbolic models checking tool, called Probabilistic Symbolic Model (PRISM). The successful applicability of PRISM in wider range of application domains motivated us to present a comparison of those applications in a precise manner. We also presented an enhanced version of Continuous-time Markov Chain (CTMC) model for evaluation of Fault Tolerant Target Tracking (FTTT) protocol implemented in wireless sensor networks. PRISM is preferred for the probabilistic modeling of FTTT protocol to aid symmetry reduction during modeling. We proceeded with probabilistic results which pinpointed the comparison of FTTT performance via PRISM, PRISM-symm and generic representatives in PRISM (GRIP) models. Modeling experiments confirmed that PRISM-symm is giving improved outcomes in comparison with PRISM and GRIP.
Index Terms—Index Terms—CTMC model, FTTT protocol, model checking, PRISM, PRISM-symm, GRIP.
S. Bhatti and M. Memon are with the Department of Software Engineering, Mehran University of Engineering and Technology, Jamshoro, Sindh, Pakistan (e-mail: sania.bhatti@faculty.muet.edu.pk, mohsin.memon@faculty.muet.edu.pk). S. Memon is with the Computer Systems Engineering Department, Mehran University of Engineering and Technology, Jamshoro, Sindh, Pakistan (e-mail: mesheeraz@hotmail.com).
[PDF]
Cite:Sania Bhatti, Mohsin Memon, and Sheeraz Memon, "Evaluating FTTT Protocol via PRISM, PRISM-symm and GRIP," International Journal of Computer Theory and Engineering vol. 9, no. 3, pp. 162-166, 2017.
