Abstract

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 project, we analyze a simple probabilistic weather forecasting model for Islamabad weather using the PRISM model checker. The reachability 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.

Different weather conditions of consecutive days

People

• Adnan Rashid, SEECS, NUST, Pakistan
• Sohail Iqbal, SEECS, NUST, Pakistan
• Asad Ahmed, SEECS, NUST, Pakistan

Publications

1. A. Ahmed, A. Rashid and S. Iqbal, “Formal Analysis of Weather Forecasting Model in PRISM”, Frontiers of Information Technology (FIT), IEEE, pp: 355-360, Islamabad, Pakistan, 2014.