Abstract
Bounded model checking (BMC) with satisfiability modulo theories (SMT) is a powerful approach for generating test cases or finding bugs. However, it is generally difficult to determine an appropriate unrolling bound k in BMC. An SMT formula for BMC might be unsatisfiable because of the insufficiency of k. In this paper, we propose a novel approach for BMC using partial maximum satisfiability, in which the initial conditions of state variables are treated as soft constraints. State variables whose initial conditions are not satisfied in the solution of a maximum satisfiability solver can be regarded as bottlenecks in BMC. We can simultaneously estimate modified initial conditions for these bottleneck variables, with which the formula becomes satisfiable. Furthermore, we propose a method based on dual slicing to delineate the program path that is changed when we modify the initial conditions of the specified bottlenecks. The analysis results help us to estimate a suitable unrolling bound. We present experimental results using examples from the automotive industry to demonstrate the usefulness of the proposed method.
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.
This is not the actual number estimated from the real model. However, the order of the unrolling bound required for the real model was the same.
References
Ansótegui, C., Bonet, M.L., Levy, J.: Sat-based maxsat algorithms. Artif. Intell. 196, 77–105 (2013)
Brillout, A., He, N., Mazzucchi, M., Kroening, D., Purandare, M., Rümmer, P., Weissenbacher, G.: Mutation-based test case generation for simulink models. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 208–227. Springer, Heidelberg (2010)
Clarke, E., Kroning, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 85–96. Springer, Heidelberg (2004)
Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252–265. Springer, Heidelberg (2006)
Gadkari, A.A., Yeolekar, A., Suresh, J., Ramesh, S., Mohalik, S., Shashidhar, K.C.: AutoMOTGen: automatic model oriented test generator for embedded control systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 204–208. Springer, Heidelberg (2008)
Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 519–531. Springer, Heidelberg (2007)
Johnson, N., Caballero, J., Chen, K., McCamant, S., Poosankam, P., Reynaud, D., Song, D.: Differential slicing: identifying causal execution differences for security applications. In: IEEE Symposium on Security and Privacy, pp. 347–362 (2011)
Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: PLDI 2011, pp. 437–446 (2011)
Kim, M., Kim, Y., Kim, H.: A comparative study of software model checkers as unit testing tools: an industrial case study. TSE 37(2), 146–160 (2011)
Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. FMSD 47(1), 75–92 (2015)
Kroning, D., Strichman, O.: Efficient computation of recurrence diameters. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 298–309. Springer, Heidelberg (2002)
Kutsuna, T., Ishii, Y., Yamamoto, A.: Abstraction and refinement of mathematical functions toward SMT-based test-case generation. Int. J. Softw. Tools Technol. Transfer 1–12 (2015)
McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 1–13. Springer, Heidelberg (2003)
Reicherdt, R., Glesner, S.: Slicing matlab simulink models. In: ICSE 2012, pp. 551–561 (2012)
Schrammel, P., Kroening, D., Brain, M., Martins, R., Teige, T., Bienmüller, T.: Successful use of incremental BMC in the automotive industry. In: Núñez, M., Güdemann, M. (eds.) Formal Methods for Industrial Critical Systems. LNCS, vol. 9128, pp. 62–77. Springer, Heidelberg (2015)
Sheeran, M., Singh, S., Stålmarck, G.: Checking safety properties using induction and a SAT-solver. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 108–125. Springer, Heidelberg (2000)
Shtrichman, O.: Pruning techniques for the SAT-based bounded model checking problem. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 58–70. Springer, Heidelberg (2001)
The MathWorks Inc. http://www.mathworks.com
Weeratunge, D., Zhang, X., Sumner, W.N., Jagannathan, S.: Analyzing concurrency bugs using dual slicing. In: ISSTA 2010, pp. 253–264 (2010)
Acknowledgement
The authors are grateful for the useful comments and support provided by Tetsuya Tohdo and Hiroyuki Ihara at DENSO CORPORATION.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Kutsuna, T., Ishii, Y. (2016). Analyzing Unsatisfiability in Bounded Model Checking Using Max-SMT and Dual Slicing. In: ter Beek, M., Gnesi, S., Knapp, A. (eds) Critical Systems: Formal Methods and Automated Verification. AVoCS FMICS 2016 2016. Lecture Notes in Computer Science(), vol 9933. Springer, Cham. https://doi.org/10.1007/978-3-319-45943-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-45943-1_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-45942-4
Online ISBN: 978-3-319-45943-1
eBook Packages: Computer ScienceComputer Science (R0)