Navegar

Colección

Datos Estadísticas

Artículo

Estamos trabajando para incorporar este artículo al repositorio
Consulte el artículo en la página del editor
Consulte la política de Acceso Abierto del editor

Abstract:

Model-based reliability estimation of systems can provide useful insights early in the development process. However, computational complexity of estimating metrics such as mean time to first failure (MTTFF), turnaround time (TAT), or other domain-based quantitative measures can be prohibitive both in time, space, and precision. In this article, we present an alternative to exhaustive model exploration, as in probabilistic model checking, and partial random exploration, as in statistical model checking. Our hypothesis is that a (carefully crafted) partial systematic exploration of a system model can provide better bounds for these quantitative model metrics at lower computation cost. We present a novel automated technique for metric estimation that combines simulation, invariant inference, and probabilistic model checking. Simulation produces a probabilistically relevant set of traces from which a state invariant is inferred. The invariant characterises a partial model, which is then exhaustively explored using probabilistic model checking. We report on experiments that suggest that metric estimation using this technique (for both fully probabilistic models and those exhibiting nondeterminism) can be more effective than (full-model) probabilistic and statistical model checking, especially for system models for which the events of interest are rare. © 2016 ACM.

Registro:

Documento: Artículo
Título:Less is more: Estimating probabilistic rewards over partial system explorations
Autor:Pavese, E.; Braberman, V.; Uchitel, S.
Filiación:Departamento de Computación, Universidad de Buenos Aires, Argentina
Departamento de Computación, Universidad de Buenos Aires, CONICET, Argentina
Departamento de Computación, Universidad de Buenos Aires, Imperial College London, CONICET, Argentina
Palabras clave:Estimation; Model checking; Partial verification; Probability; Quantitativemodelling; Estimation; Probability; Turnaround time; Mean time to first failure; Partial verification; Probabilistic model checking; Quantitative measures; Quantitativemodelling; Reliability estimation; Statistical model checking; Systematic exploration; Model checking
Año:2016
Volumen:25
Número:2
DOI: http://dx.doi.org/10.1145/2890494
Título revista:ACM Transactions on Software Engineering and Methodology
Título revista abreviado:ACM Trans. Software Eng. Methodol.
ISSN:1049331X
CODEN:ATSME
Registro:https://bibliotecadigital.exactas.uba.ar/collection/paper/document/paper_1049331X_v25_n2_p_Pavese

Referencias:

  • Aziz, A., Singhal, V., Balarin, F., Brayton, R.K., Sangiovanni-Vincentelli, A., It usually works: The temporal logic of stochastic systems (1995) Lecture Notes in Computer Science, p. 155. , Springer, Berlin
  • Baier, C., Katoen, J.P., (2008) Principles of Model Checking., , MIT Press, Cambridge, MA
  • Basu, S., Ghosh, A., He, R., Approximate model checking of PCTL involving unbounded path properties (2009) ICFEM'09, pp. 326-346
  • Bianco, A., De Alfaro, L., Model checking of probabilistic and nondeterministic systems (1995) Proceedings of Foundations of Software Technology and Theoretical Computer Science, 1026, pp. 499-513
  • Bogdoll, J., Ferrer Fioriti, L.M., Hartmanns, A., Hermanns, H., Partial order methods for statistical model checking and simulation (2011) FMOODS/FORTE., pp. 59-74
  • Borges, M., Filieri, A., D'Amorim, M., PǍsǍreanu, C.S., Visser, W., Compositional solution space quantification for probabilistic software analysis (2014) Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'14), pp. 123-132. , http://dx.doi.org/10.1145/2594291.2594329, ACM, New York, NY
  • Chernoff, H., A measure of asymptotic efficiency for tests of a hypothesis based on the sum of observations (1952) Annals of Mathematical Statistics, 23 (4), pp. 493-507
  • Clarke, E.M., Grumberg, O., Minea, M., Peled, D., State space reduction using partial order techniques (1999) International Journal on Software Tools for Technology Transfer, 2 (3), pp. 279-287
  • Coles, S., (2001) An Introduction to Statistical Modelling of Extreme Values., , Springer
  • D'Argenio, P., Jeannet, B., Jensen, H., Larsen, K., Reachability analysis of probabilistic systems by successive refinements. in PAPM/PROBMIV (2001) Lecture Notes in Computer Science, 2165, pp. 39-56. , Springer, Berlin
  • De Nicola, R., Katoen, J., Latella, D., Massink, M., Towards a logic for performance and mobility (2006) Electronic Notes in Theoretical Computer Science, 153 (2), pp. 161-175
  • Dean, T., Givan, R., Modelminimization in Markov decision processes (1997) Proceedings of TheNational Conference on Artificial Intelligence., pp. 106-111
  • Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C., The Daikon system for dynamic detection of likely invariants (2007) Science of Computer Programming., 69 (1-3), pp. 35-45
  • Filieri, A., Pasareanu, C.S., Visser, W., Reliability analysis in symbolic pathfinder (2013) 35th International Conference on Software Engineering (ICSE'13), pp. 622-631. , http://dl.acm.org/citation.cfm?id=2486870, San Francisco, CA, May 18-26 2013
  • He, R., Jennings, P., Basu, S., Ghosh, A.P., Wu, H., A bounded statistical approach for model checking of unbounded until properties (2010) Proceedings of the IEEE/ACM International Conference on Automated Software Engineering, pp. 225-234. , ACM
  • Helmink, L., Sellink, M., Vaandrager, F., Proof-checking a data link protocol (1994) Proceedings of the International Workshop on Types for Proofs and Programs (TYPES'93), Lecture Notes in Computer Science, 806. , Springer, Berlin
  • Henriques, D., Martins, J., Zuliani, P., Platzer, A., Clarke, E., Statistical model checking for Markov decision processes (2012) QEST., pp. 84-93
  • Hermanns, H., Meyer-Kayser, J., Siegle, M., Multi terminal binary decision diagrams to represent and analyse continuous time Markov chains (1999) Proceedings of NSMC'99, pp. 188-207. , Prensas Universitarias de Zaragoza
  • Hinton, A., Kwiatkowska, M., Norman, G., Parker, D., PRISM: A tool for automatic verification of probabilistic systems (2006) TACAS'06 Proceedings, Lecture Notes in Computer Science, 3920, pp. 441-444. , Springer, Berlin
  • (1997) IEEE Standard for Wireless LAN Medium Access Control (MAC) and Physical Layer (PHY) Specifications, , Institute of Electrical and Electronic Engineers
  • Jamieson, L.H., Dean, B.C., Weighted alliances in graphs (2007) Congressus Numerantium, 187, p. 76
  • Kalambi, I.B., A comparison of three iterative methods for the solution of linear equations (2008) Journal of Applied Sciences and Environmental Management, 12, p. 4
  • Katoen, J.-P., Zapreev, I.S., Moritz Hahn, E., Hermanns, H., Jansen, D.N., The ins and outs of the probabilistic model checker MRMC (2011) Performance Evaluation, 68 (2), pp. 90-104
  • Kaufman, L.M., Johnson, B.W., Dugan, J.B., Coverage estimation using statistics of the extremes for when testing reveals no failures (2002) IEEE Transactions on Computers, pp. 3-12
  • Kwiatkowska, M., Norman, G., Parker, D., Symmetry reduction for probabilistic model checking (2006) Computer Aided Verification., pp. 234-248. , Springer
  • Kwiatkowska, M., Norman, G., Parker, D., Grazia Vigliotti, M., Probabilistic mobile ambients (2009) Theoretical Computer Science, 410 (12), pp. 1272-1303
  • Guldstrand Larsen, K., Larsson, F., Pettersson, P., Yi, W., Efficient verification of real-time systems: Compact data structure and state-space reduction (1997) Proceedings of the 18th IEEE Real-Time Systems Symposium, pp. 14-24. , IEEE
  • Lassaigne, R., Peyronnet, S., Probabilistic verification and approximation (2006) ENTCS, 143, pp. 101-114
  • Luckow, K., Corina, S., Dwyer, P., Matthew, B., Filieri, A., Visser, W., Exact and approximate probabilistic symbolic execution for nondeterministic programs (2014) Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering (ASE'14), pp. 575-586. , http://dx.doi.org/10.1145/2642937.2643011, ACM, New York, NY
  • Lyu, M.R., (1996) Handbook of Software Reliability Engineering., , McGraw-Hill, Inc., Hightstown, NJ
  • Musa, J.D., Iannino, A., Okumoto, K., (1987) Software Reliability: Measurement, Prediction, Application, , McGraw-Hill, New York, NY
  • Nimal, V., (2010) Statistical Approaches for Probabilistic Model Checking, , Master's Dissertation. Oxford University Computing Laboratory, Oxford, UK
  • Pavese, E., Braberman, V., Uchitel, S., My model checker died!: How well did it do? (2010) QUOVADIS/ICSE'10, pp. 33-40. , http://dx.doi.org/10.1145/1808877.1808884, ACM
  • Pavese, E., Braberman, V., Uchitel, S., Automated reliability estimation over partial systematic explorations (2013) Proceedings of the 2013 International Conference on Software Engineering., pp. 602-611. , IEEE Press
  • Qureshi, M.A., Sanders, W.H., A new methodology for calculating distributions of reward accumulated during a finite interval (1996) Proceedings of Annual Symposium on Fault Tolerant Computing., pp. 116-125. , IEEE
  • Rabih, D., Pekergin, N., Statistical model checking using perfect simulation (2009) Proceedings of ATVA'09., pp. 120-134. , Springer
  • Reijsbergen, D., De Boer, P., Scheinhardt, W., Haverkort, B., Automated rare event simulation for stochastic petri nets (2013) Lecture Notes in Computer Science, 8054, pp. 372-388. , http://dx.doi.org/10.1007/978-3-642-40196-1_31, Quantitative Evaluation of Systems, Kaustubh Joshi, Markus Siegle, Mariëlle Stoelinga, and Pedro R. D'Argenio (Eds.), Springer, Berlin
  • Robert, C.P., Casella, G., (2005) Monte Carlo Statistical Methods., , Springer, New York, NY
  • Rubinstein, R.Y., Kroese, D.P., (2008) Simulation and the Monte Carlo Method (Series in Probability and Statistics), 707. , John Wiley & Sons, Hoboken, NJ
  • Sawilowsky, S.S., You think you've got trivials? (2003) Journal of Modern Applied Statistical Methods, 2 (1), p. 21
  • Segala, R., (1995) Modelling and Verification of Randomized Distributed Real Time Systems, , Ph.D. Dissertation. Massachusetts Institute of Technology, Cambridge, MA
  • Sen, K., Viswanathan, M., Agha, G., On statistical model checking of stochastic systems (2005) Proceedings of CAV'05., pp. 266-280. , Springer
  • Sen, K., Viswanathan, M., Agha, G., VESTA: A statistical model-checker and analyzer for probabilistic systems (2005) QEST'05., pp. 251-252. , IEEE
  • Sun, J., Liu, Y., Song Dong, J., Pang, J., PAT: Towards flexible verification under fairness (2009) Proceedings of the 21th International Conference on Computer Aided Verification (CAV'09), 5643, pp. 709-714
  • Vardi, M., Automatic verification of probabilistic concurrent finite state programs (1985) SFCS'85., pp. 327-338. , IEEE
  • Villén-Altamirano, M., Villén-Altamirano, J., RESTART: A straightforward method for fast simulation of rare events (1994) Proceedings of WSC'94, pp. 282-289. , San Diego, CA
  • Wóznicki, Z.I., On performance of {SOR} method for solving nonsymmetric linear systems (2001) Journal of Computational and Applied Mathematics, 137 (1), pp. 145-176. , http://dx.doi.org/10.1016/S0377-0427(00)00705-6
  • Younes, H., Ymer: A statistical model checker (2005) Computer Aided Verification., pp. 171-179. , Springer
  • Younes, H., Clarke, E., Zuliani, P., Statistical verification of probabilistic properties with unbounded until (2011) Formal Methods: Foundations and Applications, pp. 144-160

Citas:

---------- APA ----------
Pavese, E., Braberman, V. & Uchitel, S. (2016) . Less is more: Estimating probabilistic rewards over partial system explorations. ACM Transactions on Software Engineering and Methodology, 25(2).
http://dx.doi.org/10.1145/2890494
---------- CHICAGO ----------
Pavese, E., Braberman, V., Uchitel, S. "Less is more: Estimating probabilistic rewards over partial system explorations" . ACM Transactions on Software Engineering and Methodology 25, no. 2 (2016).
http://dx.doi.org/10.1145/2890494
---------- MLA ----------
Pavese, E., Braberman, V., Uchitel, S. "Less is more: Estimating probabilistic rewards over partial system explorations" . ACM Transactions on Software Engineering and Methodology, vol. 25, no. 2, 2016.
http://dx.doi.org/10.1145/2890494
---------- VANCOUVER ----------
Pavese, E., Braberman, V., Uchitel, S. Less is more: Estimating probabilistic rewards over partial system explorations. ACM Trans. Software Eng. Methodol. 2016;25(2).
http://dx.doi.org/10.1145/2890494