A Comparative Study of Software Model Checkers as Unit Testing Tools: An Industrial Case Study

—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. 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 ...

• Type: Journal
• Year: 2011
• Where: TSE
• Authors: Moonzoo Kim, Yunho Kim, Hotae Kim
• Keywords: Model Checkers, Software Model, Software Model Checkers, TSE 2011