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.

Flash memory has become virtually indispensable in most mobile devices, such as mobile phones, digital cameras, mp3 players, etc. In order for mobile devices to successfully provide services, it is essential that flash memory be controlled correctly through the device driver software. However, as is typical for embedded software, conventional testing methods often fail to detect hidden flaws in the complex device driver software. This deficiency incurs significant development and operation overhead to the manufacturers. As a complementary approach to improve the reliability of embedded software, model checking provides a complete analysis of a target model but the size of the target software is limited due to the state explosion problem.In this project, we have verified the correctness of a multi-sector read operation of Samsung OneNANDTM flash device driver by using both model checking and testing. We started the verification task with the model checkers NuSMV and Spin for an exhaustive analysis of a small size flash as a pre-testing step. We then set up a testbed based on a formal model used for model checking and performed testing on a large size flash. Through these verification tasks, we could successfully verify the correctness of the multi-sector read operation with both complete exploration of model checking and scalability of testing.

Flash memory has become virtually indispensable in most mobile devices. In order for mobile devices to operate successfully, it is essential that the flash memory be controlled correctly through the device driver software. However, as is typical for embedded software, conventional testing methods often fail to detect hidden flaws in the complex device driver software. This deficiency incurs significant development and operation overheads to the manufacturers. Model checking techniques have been proposed to compensate for the weaknesses of conventional testing methods through exhaustive analyses. These techniques, however, require significant manual efforts to create an abstract target model and, thus, are not widely applied in industry. In this project, we applied a model checking technique based on a Boolean satisfiability (SAT) solver. One advantage of SAT-based model checking is that a target C code can be analyzed directly without an abstract model, thereby enabling automated and bit-level accurate verification. In this project, we have applied CBMC, a SAT-based software model checker, to the unit testing of the Samsung OneNANDtrade device driver. Through this project, we detected several bugs that had not been discovered previously.