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

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.