Abstract
Formal verification methods, such as Model Checking, have been used for addressing performance/dependability analysis of systems. Such formal methods have several advantages over traditional techniques aiming at performance/dependability analysis such as the use of a single computational technique for evaluation of any measure and all complex numerical computation steps are hidden to the user. This paper reports on the use of Probabilistic Model Checking for time performance evaluation of complex systems. We propose an approach, TPerP, that allows a professional to clearly address time performance analysis based on Continuous-Time Markov Chain (CTMC). Our approach takes into consideration several types of delay analyzes. We applied it to a balloon-borne high energy astrophysics scientific experiment where we dealt with CTMCs that had around 30 million reachable states and 75 million transitions, and we concluded that the current definition used in the balloon system is inadequate in terms of performance.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Bolch, G., Greiner, S., de Meer, H., Trivedi, K.S.: Queueing Networks and Markov Chains. Jonh Wiley & Sons, New York (1998)
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76–85 (2010)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time markov chains. IEEE Trans. Softw. Eng. 29(6), 524–541 (2003)
Kwiatkowska, M., Norman, G., Parker, D.: Controller dependability analysis by probabilistic model checking. Control Eng. Pract. 15(11), 1427–1434 (2006)
Massink, M., ter Beek, M.H., Latella, D.: Towards model checking stochastic aspects of the thinkteam user interface. In: Gilroy, S.W., Harrison, M.D. (eds.) DSV-IS 2005. LNCS, vol. 3941, pp. 39–50. Springer, Heidelberg (2006)
Haverkort, B.R., Hermanns, H., Katoen, J.-P.: On the use of model checking techniques for dependability evaluation. In: Proceedings of IEEE Symposium Reliable Distributed Systems, pp. 228–237. IEEE (2000)
Grunske, L.: Specification patterns for probabilistic quality properties. In: Proceedings of the International Conference on Software Engineering, pp. 31–40. ACM (2008)
Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the International Conference on Software Engineering, pp. 411–420. ACM (1999)
Konrad, S., Cheng, B.H.C.L.: Real-time specification patterns. In: Proceedings of the International Conference on Software Engineering, pp. 372–381. ACM (2005)
Hoenicke, J., Post, A.: Formalization and analysis of real-time requirements: a feasibility study at BOSCH. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 225–240. Springer, Heidelberg (2012)
Braga, J., D’Amico, F., Avila, M.A.C., Penacchioni, A.V., Sacahui, J.R., de Santiago Jr., V.A., Mattiello-Francisco, F., Strauss, C., Fialho, M.A.A.: The protoMIRAX hard X-ray imaging balloon experiment. Astron. Astrophy. 580, A108 (2015)
Esteve, M.-A., Katoen, J.-P., Nguyen, V.Y., Postma, B., Yushtein, Y.: Formal correctness, safety, dependability, and performance analysis of a satellite. In: Proceedings of the International Conference on Software Engineering, pp. 1022–1031. IEEE Press (2012)
Bozzano, M., Cimatti, A., Katoen, J.-P., Katsaros, P., Mokos, K., Nguyen, V.Y., Noll, T., Postma, B., Roveri, M.: Spacecraft early design validation using formal methods. Reliab. Eng. Syst. Saf. 132, 20–35 (2014)
Kikuchi, S., Matsumoto, Y.: Performance modeling of concurrent live migration operations in cloud computing systems using PRISM probabilistic model checker. In: Proceedings of the IEEE International Conference on Cloud Computing, pp. 49–56. IEEE (2011)
Acknowledgments
This work was supported by a CNPq BSP grant, Institutional Process Number 455097/2013-5, Individual Process Number 170143/2014-7.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
de Santiago Júnior, V.A., Tahar, S. (2016). Time Performance Formal Evaluation of Complex Systems. In: Cornélio, M., Roscoe, B. (eds) Formal Methods: Foundations and Applications. SBMF 2015. Lecture Notes in Computer Science(), vol 9526. Springer, Cham. https://doi.org/10.1007/978-3-319-29473-5_10
Download citation
DOI: https://doi.org/10.1007/978-3-319-29473-5_10
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-29472-8
Online ISBN: 978-3-319-29473-5
eBook Packages: Computer ScienceComputer Science (R0)