Analysis of Weather Forecasting Model in PRISM

Weather forecasting provides an important information for general public. Analysis of weather forecasting models, through traditional simulation techniques, are not exhaustive and thus not accurate. Probabilistic model checking, a formal methods technique, as a complementary approach provides an accurate analysis for probabilistic models. In this paper, we have analyzed a simple probabilistic weather forecasting model for Islamabad weather using PRISM model checker. The reach ability and prediction capability of model has been analyzed using quantitative and qualitative properties in PRISM. Analysis shows that all the states of weather forecasting model are reachable and model is biased. In addition, we have also implemented this model in MATLAB and compared the results of both implementation, quantitatively. We have also presented a comparison between PRISM and MATLAB implementation of weather forecasting model, qualitatively.