Guided Model Checking with a Bayesian Meta-heuristic

• Autorzy: Seppi K. , Jones M. , Lamborn P.
• Języki publikacji: EN

Abstrakty

EN

This paper presents a meta-heuristic for use in finding errors in models of complex concurrent systems using explicit guided model checking. The meta-heuristic improves explicit guided model checking by applying the empirical Bayes method to revise heuristic estimates of the distance from a given state to an error state. Guided search using the revised estimates finds errors with less search effort than the original estimates.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 70, nr 1,2
• Strony: 111--126
• Opis fizyczny: bibliogr. tab., wykr., bibliogr. 20 poz

Twórcy

autor

Seppi K.

autor

Jones M.

autor

Lamborn P.

• Department of Computer Science, 3328 TMCB, Brigham Young University, Provo, UT 84602, USA,

Bibliografia

• [1] Bloem, R., Ravi, K., Somenzi, F.: Symbolic guided search for CTL model checking, Design Automation Conference (DAC'00), 2000.
• [2] Bradley P. Carlin, T. A. L.: Bayes and Empirical Bayes Methods for Data Analysis, Chapman & Hall, 1996.
• [3] DeGroot, M. H.: Optimal Statistical Decisions, McGraw-Hill, 1970.
• [4] Dill, D. L.: TheMuro: Verification System, Computer-Aided Verification, CAV '96 (R. Alur, T. A. Henzinger, Eds.), 1102, Springer-Verlag, New Brunswick, NJ, July/August 1996.
• [5] Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed Explicit Model Checking with HSF-SPIN, 8th International SPIN Workshop on Model Checking Software, number 2057 in Lecture Notes in Computer Science, Springer-Verlag, 2001.
• [6] Groce, A., Visser, W.: Model Checking Java Programs using Structural Heuristics, International Symposium on Software Testing and Analysis, July 2002.
• [7] Hansson, O., Mayer, A.: Probabilistic heuristic estimates, Annals of Mathematics and Artificial Intelligence, 2, 1990, 209-220.
• [8] Hart, P., Nilsson, N., Raphael, B.: A formal basis for the heuristic determination of minimum cost paths, IEEE Transactions on Systems, Science and Cybernetics, SSC-4(2), 1968, 100-107.
• [9] Holzer,M., Schwoon, S.: Assembling molecules in atomix is hard, Technical Report TUM-I0101, Institut für Informatik, Technische Universität München, June 2001.
• [10] Hueffner, F., Edelkamp, S., Fernau, H., Niedermeier, R.: Finding optimal solutions to Atomix, Proceedings of the Joint German/Austrian Conference on Artificial Intelligence, 24th German / 9th Austrian Conference on Artificial Intelligence (KI 2001), number 2174 in Lecture Notes in Artificial Intelligence, Springer, 2001.
• [11] Jones, M. D., Sorber, J.: Parallel search for LTL violations, Software Tools for Technology Transer, 7(1), 2005, 31-42.
• [12] Maritz, J.: Emperical Bayes Methods, Methuen, 1970.
• [13] Morris, C. N.: Parametric empirical Bayes inference: theory and applications. With discussion, Journal of the American Statistical Association, 78(381), 1983, 47-65.
• [14] Morris, C. N., Efron, B.: Empirical Bayes Estimators on Vector Observations - An Extension of Stein's Method, Biometrika, 59, 1972, 335-347.
• [15] Pelanek, R.: Typical Structural Properties of State Spaces, International SPIN Workshop on Software Model Checking (SPIN'04), number 2989 in LNCS, Springer, Barcelona, Spain, March 2004.
• [16] Pyhälä, T., Heljanko, K.: Specification Coverage Aided Test Selection, Proceeding of the 3rd International Conference on Application of Concurrency to System Design (ACSD'2003) (J. Lilius, F. Balarin, R. J. Machado, Eds.), IEEE Computer Society, June 2003.
• [17] Seppi, K.: Empirical Bayes Assisted Probabilistic Search, Technical Report VV-0301, Brigham Young University Department of Computer Science, 2003.
• [18] Seppi, K., Jones, M., Lamborn, P.: Guided Model Checking with a Bayesian Meta-heuristic, Applications of Concurrency to System Design (ACSD'04), Hamilton, Ontario, Canada, June 2004.
• [19] Stein, C.: Inadmissibility of the usual estimator for the mean of a multivariate normal distribution, Proc. Of Third Berkeley Symposium on Mathematical Statistics and Probability 1, U. of California Press, 1955.
• [20] Yang, C., Dill, D.: Validation with guided search fo the state space, 35th Design Automation Conference (DAC98), 1998.