Subscribe

Issue No.02 - March/April (2011 vol.37)

pp: 146-160

Moonzoo Kim , KAIST, Daejon

Yunho Kim , KAIST, Daejon

Hotae Kim , Samsung Electronics, Suwon

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2010.68

ABSTRACT

Conventional testing methods often fail to detect hidden flaws in complex embedded software such as device drivers or file systems. This deficiency incurs significant development and support/maintenance cost for the manufacturers. Model checking techniques have been proposed to compensate for the weaknesses of conventional testing methods through exhaustive analyses. Whereas conventional model checkers require manual effort to create an abstract target model, modern software model checkers remove this overhead by directly analyzing a target C program, and can be utilized as unit testing tools. However, since software model checkers are not fully mature yet, they have limitations according to the underlying technologies and tool implementations, potentially critical issues when applied in industrial projects. This paper reports our experience in applying Blast and CBMC to testing the components of a storage platform software for flash memory. Through this project, we analyzed the strong and weak points of two different software model checking technologies in the viewpoint of real-world industrial application—counterexample-guided abstraction refinement with predicate abstraction and SAT-based bounded analysis.

INDEX TERMS

Embedded software verification, software model checking, bounded model checking, CEGAR-based model checking, flash file systems.

CITATION

Moonzoo Kim, Yunho Kim, Hotae Kim, "A Comparative Study of Software Model Checkers as Unit Testing Tools: An Industrial Case Study",

*IEEE Transactions on Software Engineering*, vol.37, no. 2, pp. 146-160, March/April 2011, doi:10.1109/TSE.2010.68REFERENCES

- [1] CREST—Automatic Test Generation Tool for C, http://code. google.com/pcrest/, 2010.
- [2] Flash Memory (from Wikipedia), http://en.wikipedia.org/wikiFlash_memory , 2010.
- [3] Samsung OneNAND Fusion Memory, http://www. samsung.com/global/business/ semiconductor/products/ fusionmemory Products_OneNAND.html, 2010.
- [4]
Proc. 12th Int'l Conf. Theory and Applications of Satisfiability Testing, 2009.- [5] T. Ball, B. Cook, V. Levin, and S.K. Rajamani, “Slam and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft,”
Proc. Int'l Conf. Integrated Formal Methods, 2004.- [6] T. Ball, R. Majumdar, T. Millstein, and S.K. Rajamani, “Automatic Predicate Abstraction of c Programs,”
Proc. Conf. Programming Language Design and Implementation, 2001.- [7] T. Ball and S.K. Rajamani, “Automatically Validating Temporal Safety Properties of Interfaces,”
Proc. Spin Workshop, pp. 103-122, 2001.- [8] D. Beyer, T. Henzinger, R. Jhala, and R. Majumdar, “The Software Model Checker Blast: Applications to Software Engineering,”
Int'l J. Software Tools for Technology Transfer, vol. 9, pp. 505-525, 2007.- [9] D. Beyer, D. Zufferey, and R. Majumdar, “CSIsat: Interpolation for LA+EUF,”
Proc. Int'l Conf. Computer Aided Verification, 2008.- [10] A. Biere, A. Cimatti, E. Clarke, O. Strichman, and Y. Zhu, “Bounded Model Checking,”
Advances in Computers, vol. 58, pp. 117-148, 2003.- [11] A. Butterfield, L. Freitas, and J. Woodcock, “Mechanising a Formal Model of Flash Memory,”
Science of Computer Programming, vol. 74, no. 4, pp. 219-237, 2009.- [12] C. Cadar, D. Dunbar, and D. Engler, “KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs,”
Proc. Conf. Operating System Design and Implementation, 2008.- [13] C. Cadar, V. Ganesh, P.M. Pawlowski, D.L. Dill, and D.R. Engler, “EXE: Automatically Generating Inputs of Death,”
Proc. ACM Conf. Computer and Comm. Security, 2006.- [14] S. Chaki, E. Clarke, A. Groce, S. Jha, and H. Veith, “Modular Verification of Software Components in C,”
IEEE Trans. Software Eng., vol. 30, no. 6, pp. 388-402, June 2004.- [15] A. Chakrabarti, L. de Alfaro, T. Henzinger, M. Jurdzínski, and F. Mang, “Interface Compatibility Checking for Software Modules,”
Proc. Int'l Conf. Computer Aided Verification, 2001.- [16] A. Cimatti, A. Griggio, and R. Sebastiani, “Efficient Interpolant Generation in Satisfiability Modulo Theories,”
Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2008.- [17] E. Clarke, A. Biere, R. Raimi, and Y. Zhu, “Bounded Model Checking Using Satisfiability Solving,”
Formal Methods in System Design, vol. 19, no. 1, pp. 7-34, 2001.- [18] E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, “Counter Example-Guided Abstraction Refinement for Symbolic Model Checking,”
J. ACM, vol. 50, no. 5, pp. 752-794, 2003.- [19] E. Clarke, D. Kroening, and F. Lerda, “A Tool for Checking ANSI-C Programs,”
Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2004.- [20] E. Clarke, D. Kroening, N. Sharygina, and K. Yorav, “Predicate Abstraction of ANSI-C Programs Using SAT,”
Formal Methods in System Design, vol. 25, nos. 2/3, pp. 105-127, 2004.- [21] E. Clarke, D. Kroening, N. Sharygina, and K. Yorav, “SATABS: SAT-Based Predicate Abstraction for ANSI-C,”
Proc. Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, 2005.- [22] B. Cook, D. Kroening, and N. Sharygina, “Cogent: Accurate Theorem Proving for Program Verification,”
Proc. Int'l Conf. Computer Aided Verification, 2005.- [23] P. Cousot, “Abstract Interpretation,”
ACM Computing Surveys, vol. 28, no. 2, pp. 324-328, 1996.- [24] D. Detlefs, G. Nelson, and J.B. Saxe, “Simplify: A Theorem Prover for Program Checking,”
J. ACM, vol. 52, no. 3, pp. 365-473, 2005.- [25] V. D'Silva, D. Kroening, and G. Weissenbacher, “A Survey of Automated Techniques for Formal Software Verification,”
IEEE Trans. Computer-Aided Design of Integrated Circuits and Systems, vol. 27, no. 7, pp. 1165-1178, July 2008.- [26] E. Clarke, O. Grumberg, and D.A. Peled,
Model Checking. MIT Press, Jan. 2000.- [27] N. Eén and N. Sörensson, “An Extensible SAT-Solver,”
Proc. Int'l Conf. Theory and Applications of Satisfiability Testing, 2003.- [28] M.A. Ferreira, S.S. Silva, and J.N. Oliveira, “Verifying Intel Flash File System Core Specification,”
Proc. Fourth VDM-Overture Workshop, 2008.- [29] E. Gal and S. Toledo, “Algorithms and Data Structures for Flash Memories,”
ACM Computing Surveys, vol. 37, no. 2, pp. 138-163, 2005.- [30] P. Godefroid, N. Klarlund, and K. Sen, “DART: Directed Automated Random Testing,”
Proc. Conf. Programming Language Design and Implementation, 2005.- [31] S. Graf and H. Saidi, “Construction of Abstract State Graphs with PVS,”
Proc. Int'l Conf. Computer Aided Verification, pp. 72-83, 1997.- [32] A. Groce, G. Holzmann, R. Joshi, and R.G. Xu, “Putting Flight Software through the Paces with Testing, Model Checking, and Constraint-Solving,”
Proc. Workshop Constraints in Formal Verification, 2008.- [33] J. Gu, P.W. Purdom, J. Franco, and B.W. Wah, “Algorithms for the Satisfiability (SAT) Problem: A Survey,”
Satisfiability Problem: Theory and Applications, Am. Math. Soc., 1996.- [34] R. Jhala and R. Majumdar, “Software Model Checking,”
ACM Computing Surveys, vol. 41, no. 4, pp. 21-74, 2009.- [35] R. Joshi and G. Holzmann, “A Mini-Challenge: Build a Verifiable Filesystem,”
Proc. Int'l Conf. Verified Software: Theories, Tools, Experiments, 2005.- [36] E. Kang and D. Jackson, “Formal Modeling and Analysis of a Flash File System in Alloy,”
Abstract State Machines, B and Z, Springer, 2008.- [37] M. Kim, Y. Choi, Y. Kim, and H. Kim, “Formal Verification of a Flash Memory Device Driver—An Experience Report,”
Proc. Spin Workshop, 2008.- [38] M. Kim and Y. Kim, “Concolic Testing of the Multi-Sector Read Operation for Flash Memory File System,”
Proc. Brazilian Symp. Formal Methods, 2009.- [39] M. Kim, Y. Kim, and H. Kim, “Unit Testing of Flash Memory Device Driver through a SAT-Based Model Checker,”
Proc. IEEE/ACM Int'l Conf. Automated Software Eng., Sept. 2008.- [40] E. Kolb, O. Sery, and R. Weiss, “Applicability of the Blast Model Checker: An Industrial Case Study,”
Proc. Conf. Perspectives of System Informatics, 2009.- [41] K. Ku, T.E. Hart, M. Chechik, and D. Lie, “A Buffer Overflow Benchmark for Software Model Checkers,”
Proc. Int'l Conf. Automated Software Eng., 2007.- [42] W. Mahnke, S.H. Leitner, and M. Damm,
OPC Unified Architecture. Springer, 2009.- [43] K.L. McMillan, “Interpolation and SAT-Based Model Checking,”
Proc. Int'l Conf. Computer Aided Verification, 2003.- [44] K.L. McMillan, “An Interpolating Theorem Prover,”
Theoretical Computer Science, vol. 345, no. 1, pp. 101-121, 2005.- [45] J.T. Muhlberg and G. Luttgen, “BLASTing Linux Code,”
Proc. Int'l Workshop Formal Methods for Industrial Critical Systems, 2006.- [46] H. Post and W. Küchlin, “Integrated Static Analysis for Linux Device Driver Verification,”
Proc. Int'l Conf. Integrated Formal Methods, 2007.- [47] H. Post, C. Sinz, A. Kaiser, and T. Gorges, “Reducing False Positives by Combining Abstract Interpretation and Bounded Model Checking,”
Proc. Int'l Conf. Automated Software Eng., 2008.- [48] B. Schlich and S. Kowalewski, “Model Checking c Source Code for Embedded Systems,”
Software Tools for Technology Transfer, vol. 11, no. 3, pp. 187-202, 2009.- [49] K. Sen, D. Marinov, and G. Agha, “CUTE: A Concolic Unit Testing Engine for C,”
Proc. European Software Eng. Conf./Foundations of Software Eng., 2005.- [50] M. Sheeran, S. Singh, and G. Stalmarck, “Checking Safety Properties Using Induction and a SAT-Solver,”
Proc. Int'l Conf. Formal Methods in Computer Aided Design, 2000.- [51] M. Utting and B. Legeard,
Practical Model-Based Testing: A Tools Approach. Morgan Kaufmann, 2007.- [52] J. Yang, P. Twohey, D. Engler, and M. Musuvathi, “Using Model Checking to Find Serious File System Errors,”
Proc. Symp. Operating System Design and Implementation, 2004.- [53] L. Zhang and S. Malik, “The Quest for Efficient Boolean Satisfiability Solvers,”
Proc. Int'l Conf. Computer Aided Verification, 2002.- [54] H. Zhu, P.A.V. Hall, and J.H.R. May, “Software Unit Test Coverage and Adequacy,”
ACM Computing Surveys, vol. 29, no. 4, pp. 366-427, 1997. |