An Extension For PRISM Model Checker To Reduce Computation Time For Steady State Probability Analysis

Stochastic modeling is extensively used for performance analysis of systems like telecommunication, computer communication, network traffic control, etc. For many decades, this modeling technique is utilized in analyzing the performance properties of real time streaming systems like throughput, latency, jitter, error rate, etc. Continuous Time Markov Chain(CTMC) is the most used modeling approach for steady state analysis of real time streaming systems. PRISM is a probabilistic model checker tool that supports CTMC models and performs steady state analysis using Continuous Stochastic Logic(CSL). However, for the large real time streaming systems, the PRISM tool takes an enormous amount of time for calculating the steady state probability for each instance of the system's state. To address this issue, we propose a tool named Steady State Probability Analyzer(STPA), an extension for the PRISM model checker tool to perform steady state analysis in bounded time.