Comparative Study on Software Model Checkers as Unit Testing Tools based on an Industrial Case Study

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 operation overhead to 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. Since software model checkers are not fully mature yet, however, they have limitations according to the underlying technologies and tool implementations, potentially critical issues when applied to industrial projects.

We report our experience of 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 and bounded analysis based on SAT and SMT technologies.

Short bio

Moonzoo Kim received his PhD degree from the department of computer and information science at University of Pennsylvania in 2001. After graduation, he joined Samsung SECUi.COM and worked on network security appliances based on network processors for 2 years. Then, he moved to POSTECH as a post doc and joined the faculty of CS dept KAIST in 2006. His research interests include formal methods, software analysis and embedded software.

Resources

• talk slide