Abstract
This paper presents an Android app supporting the construction and compact representation of continuous probability distributions. Its intuitive drag-and-drop approach considerably eases an often delicate modelling step in model-based performance and dependability evaluation, stochastic model checking, as well in the quantitative study of system-level concurrency phenomena. To compress the size of the representations, the app connects to a web service that implements an efficient compression algorithm, which constitutes the core technological innovation behind the approach. The app enables interested users to perform rapid experiments with this technology. From a more general perspective, this approach might pioneer how web service and app technology can provide a convenient vehicle for promoting and evaluating computer aided verification innovations.
This work is partly supported by the DFG as part of SFB/TR 14 AVACS, by the EU FP7 grants 295261 (MEALS) and 318490 (SENSATION), and by the CAS/SAFEA International Partnership Program for Creative Research Teams.
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
Notes
- 1.
For statistical model checking and discrete event simulation the problem lies in the solution time needed, while for stochastic model checking it is both time and space.
References
Arnold, F., Hermanns, H., Pulungan, R., Stoelinga, M.: Time-dependent analysis of attacks. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 285–305. Springer, Heidelberg (2014)
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time Markov chains. IEEE Trans. Software Eng. 29(6), 524–541 (2003)
Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76–85 (2010). Sept
Benlian, A., Hess, T., Buxmann, P.: Drivers of SaaS-adoption an empirical study of different application types. Business & Information Systems Engineering 1(5), 357–369 (2009)
Boudali, H., Crouzen, P., Stoelinga, M.: A rigorous, compositional, and extensible framework for dynamic fault tree analysis. IEEE Trans. Depend. Sec. Comput. 7(2), 128–143 (2010)
Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. Journal of Applied Probability 31, 59–75 (1994)
Chaki, S., Schallhart, C., Veith, H.: Verification across intellectual property boundaries. ACM Trans. Softw. Eng. Methodol. 22(2), 15 (2013)
Courtney, T., Gaonkar, S., Keefe, K., Rozier, E., Sanders, W.H.: Möbius 2.3: an extensible tool for dependability, security, and performance evaluation of large and complex system models. In: DSN, pp. 353–358. IEEE (2009)
Crouzen, P., Lang, F.: Smart reduction. In: Giannakopoulou, D., Orejas, F. (eds.) FASE 2011. LNCS, vol. 6603, pp. 111–126. Springer, Heidelberg (2011)
Dugan, J.B., Bavuso, S.J., Boyd, M.A.: Dynamic fault-tree models for fault-tolerant computer systems. IEEE Trans. Reliab. 41(3), 363–377 (1992)
Horváth, A., Telek, M.: PhFit: a general phase-type fitting tool. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol. 2324, pp. 82–91. Springer, Heidelberg (2002)
Johnson, M.A., Taaffe, M.R.: The denseness of phase distributions. School of Industrial Engineering Research Memoranda, pp. 88–20. Purdue University (1988)
Kaplan, F.: Are gesture-based interfaces the future of human computer interaction? In: ICMI 2009, pp. 239–240. ACM (2009)
Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Roşu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010)
Neuts, M.F.: Matrix-Geometric Solutions in Stochastic Models: an Algorithmic Approach. Dover, Baltimore (1981)
Pulungan, R., Hermanns, H.: Acyclic minimality by construction–almost. In: QEST, pp. 63–72. IEEE Computer Society (2009)
Pulungan, R., Hermanns, H.: A construction and minimization service for continuous probability distributions. STTT 17(1), 77–90 (2015)
Thümmler, A., Buchholz, P., Telek, M.: A novel approach for phase-type fitting with the EM algorithm. IEEE Trans. Depend. Sec. Comput. 3(3), 245–258 (2006)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Bungert, M., Hermanns, H., Pulungan, R. (2015). A Compression App for Continuous Probability Distributions. In: Campos, J., Haverkort, B. (eds) Quantitative Evaluation of Systems. QEST 2015. Lecture Notes in Computer Science(), vol 9259. Springer, Cham. https://doi.org/10.1007/978-3-319-22264-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-22264-6_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-22263-9
Online ISBN: 978-3-319-22264-6
eBook Packages: Computer ScienceComputer Science (R0)