Reliability of Run-Time Quality-of-Service evaluation using parametric model checking

ABSTRACT

Run-time Quality-of-Service (QoS) assurance is crucial for business-critical systems. Complex behavioral performance metrics (PMs) are useful but often difficult to monitor or measure. Probabilistic model checking, especially parametric model checking, can support the computation of aggregate functions for a broad range of those PMs. In practice, those PMs may be defined with parameters determined by run-time data. In this paper, we address the reliability of QoS evaluation using parametric model checking. Due to the imprecision with the instantiation of parameters, an evaluation outcome may mislead the judgment about requirement violations. Based on a general assumption of run-time data distribution, we present a novel framework that contains light-weight statistical inference methods to analyze the reliability of a parametric model checking output with respect to an intuitive criterion. We also present case studies in which we test the stability and accuracy of our inference methods and describe an application of our framework to a cloud server management problem.

References

1. Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008.
2. Albert Benveniste, Claude Jard, Ajay Kattepur, Sidney Rosario, and JohnA. Thywissen. QoS-aware management of monotonic service orchestrations. Formal Methods in System Design, 44(1):1--43, 2014.
3. Radu Calinescu, Carlo Ghezzi, Kenneth Johnson, Mauro Pezzé, Yasmin Rafiq, and Giordano Tamburrelli. Formal verification with confidence intervals: A new approach to establishing the Quality-of-Service properties of software systems. Reliability, IEEE Transactions on, 2015.
4. Radu Calinescu, Lars Grunske, Marta Z. Kwiatkowska, Raffaela Mirandola, and Giordano Tamburrelli. Dynamic qos management and optimization in service-based systems. IEEE Trans. Software Eng., 37(3):387--409, 2011.
5. Radu Calinescu and Marta Kwiatkowska. Using quantitative analysis to implement autonomic it systems. In Proceedings of the 31st International Conference on Software Engineering, ICSE'09, pages 100--110, Washington, DC, USA, 2009. IEEE Computer Society.
6. Taolue Chen, E. M. Hahn, Tingting Han, M. Kwiatkowska, Hongyang Qu, and Lijun Zhang. Model repair for Markov Decision Processes. In Theoretical Aspects of Software Engineering (TASE), 2013 International Symposium on, pages 85--92, 2013.
7. Shang-Wen Cheng, David Garlan, and Bradley Schmerl. Architecture-based self-adaptation in the presence of multiple objectives. In ICSE 2006 Workshop on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), Shanghai, China, 21--22 2006.
8. Conrado Daws. Symbolic and parametric model checking of discrete-time Markov chains. In Proceedings of the First International Conference on Theoretical Aspects of Computing, ICTAC'04, pages 280--294, Berlin, Heidelberg, 2005. Springer-Verlag.
9. Antonio Filieri, Lars Grunske, and Alberto Leva. Lightweight adaptive filtering for efficient learning and updating of probabilistic models. In Proceedings of the 37th International Conference on Software Engineering, ICSE'15. IEEE, 2015.
10. Antonio Filieri, Giordano Tamburrelli, and Carlo Ghezzi. Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. Software Engineering, IEEE Transactions on, 42(1):75--99, 2016.
11. Carlo Ghezzi, Leandro Sales Pinto, Paola Spoletini, and Giordano Tamburrelli. Managing non-functional uncertainty via model-driven adaptivity. In Proceedings of the 2013 International Conference on Software Engineering, ICSE'13, pages 33--42. IEEE Press, 2013.
12. Robert Givan, Sonia M. Leach, and Thomas L. Dean. Bounded-parameter markov decision processes. Artif. Intell., 122(1-2):71--109, 2000.
13. Lars Grunske. Specification patterns for probabilistic quality properties. In Proceedings of the 30th International Conference on Software Engineering, ICSE '08, pages 31--40, New York, NY, USA, 2008. ACM.
14. Ernst Moritz Hahn, Holger Hermanns, and Lijun Zhang. Probabilistic reachability for parametric Markov models. International Journal on Software Tools for Technology Transfer, 13(1):3--19, 2011.
15. Hans Hansson and Bengt Jonsson. A logic for reasoning about time and reliability. Formal aspects of computing, 6(5):512--535, 1994.
16. Thomas Hérault, Richard Lassaigne, Frédéric Magniette, and Sylvain Peyronnet. Approximate probabilistic model checking. In Verification, Model Checking, and Abstract Interpretation, pages 73--84. Springer, 2004.
17. Robert Vincent Hogg, Joseph W. McKean, and Allen Thornton Craig. Introduction to Mathematical Statistics (6th ed). Pearson Prentice Hall, 2005.
18. Paul Jennings, Arka P. Ghosh, and Samik Basu. A two-phase approximation for model checking probabilistic unbounded until properties of probabilistic systems. ACM Trans. Softw. Eng. Methodol., 21(3):18:1--18:35, July 2012.
19. Kyriakos Kritikos, Barbara Pernici, Pierluigi Plebani, Cinzia Cappiello, Marco Comuzzi, Salima Benrernou, Ivona Brandic, Attila Kertész, Michael Parkin, and Manuel Carro. A survey on service quality description. ACM Comput. Surv., 46(1):1:1--1:58, July 2013.
20. M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real-time systems. In Proc. 23rd International Conference on Computer Aided Verification (CAV'11), pages 585--591. Springer, 2011.
21. Arnab Nilim and Laurent El Ghaoui. Robust control of Markov Decision Processes with uncertain transition matrices. Operations Research, 53(5):780--798, 2005.
22. Alberto Puggelli, Wenchao Li, Alberto L. Sangiovanni-Vincentelli, and Sanjit A. Seshia. Polynomial-time verification of PCTL properties of MDPs with convex uncertainties. In Computer Aided Verification, pages 527--542. Springer, 2013.
23. Genaína Rodrigues, David Rosenblum, and Sebastian Uchitel. Using scenarios to predict the reliability of concurrent component-based software systems. In Proceedings of the 8th International Conference on Fundamental Approaches to Software Engineering, FASE'05, pages 111--126, Berlin, Heidelberg, 2005. Springer-Verlag.
24. Koushik Sen, Mahesh Viswanathan, and Gul Agha. Model-checking Markov chains in the presence of uncertainties. In Tools and Algorithms for the Construction and Analysis of Systems, pages 394--410. Springer, 2006.
25. Guoxin Su, Taolue Chen, Yuen Feng, David S. Rosenblum, and P. S. Thiagarajan. An iterative decision-making scheme for markov decision processes and its application to self-adaptive systems. In Proceedings of the 19th International Conference on Fundamental Approaches to Software Engineering, FASE'16, Eindhoven, the Netherlands, 2016. Springer.
26. Guoxin Su, Yuan Feng, Taolue Chen, and David S. Rosenblum. Asymptotic perturbation bounds for probabilistic model checking with empirically determined probability parameters. IEEE Transactions on Software Engineering, in press.
27. Guoxin Su and David S. Rosenblum. Nested reachability approximation for discrete-time markov chains with univariate parameters. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3-7, 2014, Proceedings, pages 364--379, 2014.
28. Guoxin Su and David S. Rosenblum. Perturbation analysis of stochastic systems with empirical distribution parameters. In Proceeding of the 36th International Conference on Software Engineering (ICSE'14), 2014.
29. Anton Tarasyuk, Elena Troubitsyna, and Linas Laibinis. Formal modelling and verification of service-oriented systems in probabilistic event-b. In John Derrick, Stefania Gnesi, Diego Latella, and Helen Treharne, editors, Integrated Formal Methods - 9th International Conference, IFM 2012, Pisa, Italy, June 18-21, 2012, volume 7321 of Lecture Notes in Computer Science, pages 237--252. Springer, 2012.
30. Ambuj Tewari and Peter L. Bartlett. Bounded parameter Markov Decision Processes with average reward criterion. In Nader H. Bshouty and Claudio Gentile, editors, COLT, volume 4539 of Lecture Notes in Computer Science, pages 263--277. Springer, 2007.
31. Håkan L. S. Younes and Reid G Simmons. Statistical probabilistic model checking with a focus on time-bounded properties. Information and Computation, 204(9):1368--1409, 2006.

Index Terms

• Mathematics of computing

  • Probability and statistics

    • Multivariate statistics

    • Stochastic processes

      • Markov processes

• Software and its engineering

  • Software organization and properties

    • Software functional properties

      • Formal methods

    • Software system structures

      • Software system models

        • State systems