Abstract
Abstraction in model checking is the most effective method to overcome the state explosion problem, the most serious problem in model checking when the size and the complexity of the system-under-check are increasing. Unfortunately, when the abstraction goes wrong, the answer must be validated with the concrete system, so it faces the state explosion problem again. Moreover, the techniques in checking the abstraction and in validating must not be obstructions in the checking process. Research recently has shown that, the way to abstract a model and the approach to use abstraction are the main concerns in abstraction model checking.
In this work, we report our study on both two questions: (1) a model analyzing method to find a way of abstraction effectively, and (2) an error refinement approach using multiple abstraction in symbolic model checking. The experimentation shows that the new approach has a great performance in checking both ‘buggy‘ and ‘correct‘ models.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Menzies, T., Owen, D., Richardson, J.: The strangest thing about software. IEEE Computer 40(1), 54–60 (2007)
Qian, K., Nymeyer, A.: Abstraction-based model checking using heuristical refinement. In: Wang, F. (ed.) ATVA 2004. LNCS, vol. 3299, pp. 165–178. Springer, Heidelberg (2004)
Qian, K., Nymeyer, A., Susanto, S.: Experiments with multiple abstraction heuristics in symbolic verification. In: Zucker, J.-D., Saitta, L. (eds.) SARA 2005. LNCS (LNAI), vol. 3607, pp. 290–304. Springer, Heidelberg (2005)
Edelkamp, S., Lluch Lafuente, A., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57–79. Springer, Heidelberg (2001)
Bui, T.H., Dang, P.B.K.: Yet another variable dependency analysis for abstraction guided model checking. In: Proc. SEATUC 2012 (March 2012)
Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. In: Proc. the 5th Annual IEEE Symp. on Logic in Computer Science, pp. 1–33. IEEE Computer Society Press, Washington, D.C (1990)
Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. In: Proc. the 19th ACM SIGPLAN-SIGACT Sym. on Principles of Programming Languages, pp. 343–354 (1992)
He, F., Song, X., Hung, W.N., Gu, M., Sun, J.: Integrating evolutionary computation with abstraction refinement for model checking. IEEE Transactions on Computers 59(1), 116–126 (2010)
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proc. the ACM SIGPLAN 2001 Conf. on Programming Language Design and Implementation, pp. 203–213. ACM Press (2001)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. the 29th SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 58–70. ACM (2002)
Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994)
Eén, N., Sörensson, N.: Temporal induction by incremental SAT solving. In: Strichman, O., Biere, A. (eds.) Electronic Notes in Theoretical Computer Science, vol. 89, Elsevier (2004)
Brin, S., Page, L.: The anatomy of a large-scale hypertextual web search engine. In: Seventh International World-Wide Web Conference, WWW 1998 (1998)
Bui, T.H., Nymeyer, A.: Heuristic sensitivity in guided random-walk based model checking. In: Proc. the 7th IEEE Int. Conf. on Software Engineering and Formal Methods (SEFM 2009), pp. 125–134. IEEE Computer Society (November 2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 IFIP International Federation for Information Processing
About this paper
Cite this paper
Nguyen, P.T.H., Bui, T.H. (2014). A Multiple Refinement Approach in Abstraction Model Checking. In: Saeed, K., Snášel, V. (eds) Computer Information Systems and Industrial Management. CISIM 2015. Lecture Notes in Computer Science, vol 8838. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-45237-0_40
Download citation
DOI: https://doi.org/10.1007/978-3-662-45237-0_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-45236-3
Online ISBN: 978-3-662-45237-0
eBook Packages: Computer ScienceComputer Science (R0)