Towards accurate probabilistic models using state refinement

ABSTRACT

Probabilistic models are useful in the analysis of system behaviour and non-functional properties. Reliable estimates and measurements of probabilities are needed to annotate behaviour models in order to generate accurate predictions. However, this may not be sufficient, and may still lead to inaccurate results when the system model does not properly reflect the probabilistic choices made by the environment. Thus, not only should the probabilities be accurate in properly reflecting reality, but also the model that is being used. In this paper we identify and illustrate this problem showing that it can lead to inaccuracies and both false positive and false negative property checks. We propose state refinement as a technique to mitigate this problem, and present a framework for iteratively improving the accuracy of a probabilistically annotated behaviour model.

REFERENCES

• 1: L. Cheung, R. Roshandel, N. Medvidovic, and L. Golubchik. Early prediction of software component reliability. In ICSE '08: Proceedings of the 30th international conference on Software engineering, pages 111--120, Leipzig, Germany, 2008. ACM.
• 2: P. R. D'Argenio, B. Jeannet, H. E. Jensen, and K. G. Larsen. Reachability analysis of probabilistic systems by successive refinements. In PAPM-PROBMIV '01, pages 39--56, Aachen, Germany, 2001. Springer-Verlag.
• 3: I. Epifani, C. Ghezzi, R. Mirandola, and G. Tamburrelli. Model evolution by run-time adaptation. In ICSE '09: Proceedings of the 31st International Conference on Software engineering, Vancouver, Canada, 2009. ACM.
• 4: M. Kwiatkowska, G. Norman, and D. Parker. Prism 2.0: A tool for probabilistic model checking. In QEST '04: Proceedings of the The Quantitative Evaluation of Systems, pages 322--323, Enschede, The Netherlands, 2004. IEEE Computer Society.
• 5: P. H. Maia, J. Kramer, S. Uchitel, and N. C. Mendonça. An approach to improve accuracy in probabilistic models using state refinement. Technical report, Department of Computing, Imperial College London, 2009.
• 6: G. Rodrigues, D. Rosemblum, and S. Uchitel. Using scenarios to predict the reliability of concurrent component-based software systems. In FASE'05 / ETAPS 2005: 8th International Conference on Fundamental Approaches to Software Engineering, pages 111--126, Edinburgh, Scotland, 2005.
• 7: J. A. Whittaker and M. G. Thomason. A markov chain model for statistical software testing. IEEE Trans. Softw. Eng., 20(10):812--824, 1994.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Validation; Statistical methods

General Terms:
Design, Measurement, Theory, Verification

Keywords:
accuracy, behaviour model, probabilistic model checking, refinement