TY - JOUR
T1 - Concolic testing of the multi-sector read operation for flash storage platform software
AU - Kim, Moonzoo
AU - Kim, Yunho
AU - Choi, Yunja
PY - 2012/5
Y1 - 2012/5
N2 - In today's information society, flash memory has become a virtually indispensable component, particularly for mobile devices. In order for mobile devices to operate successfully, it is essential that flash memory be controlled correctly through flash storage platform software such as the file system, flash translation layer, and low-level device drivers. However, as is typical for embedded software, conventional testing methods often fail to detect hidden flaws in the software due to the difficulty of creating effective test cases. As a different approach, model checking techniques guarantee a complete analysis, but only on a limited scale. In this paper, we describe an empirical study wherein a concolic testing method is applied to the multi-sector read operation for flash storage platform software. This method combines a concrete dynamic execution and a symbolic execution to automatically generate test cases for full path coverage. Through the experiments, we analyze the advantages and weaknesses of the concolic testing approach on the flash storage platform software.
AB - In today's information society, flash memory has become a virtually indispensable component, particularly for mobile devices. In order for mobile devices to operate successfully, it is essential that flash memory be controlled correctly through flash storage platform software such as the file system, flash translation layer, and low-level device drivers. However, as is typical for embedded software, conventional testing methods often fail to detect hidden flaws in the software due to the difficulty of creating effective test cases. As a different approach, model checking techniques guarantee a complete analysis, but only on a limited scale. In this paper, we describe an empirical study wherein a concolic testing method is applied to the multi-sector read operation for flash storage platform software. This method combines a concrete dynamic execution and a symbolic execution to automatically generate test cases for full path coverage. Through the experiments, we analyze the advantages and weaknesses of the concolic testing approach on the flash storage platform software.
KW - And embedded software verification
KW - Concolic testing
KW - Flash memory
KW - Unit analysis
UR - http://www.scopus.com/inward/record.url?scp=84861570295&partnerID=8YFLogxK
U2 - 10.1007/s00165-011-0200-9
DO - 10.1007/s00165-011-0200-9
M3 - Article
AN - SCOPUS:84861570295
SN - 0934-5043
VL - 24
SP - 355
EP - 374
JO - Formal Aspects of Computing
JF - Formal Aspects of Computing
IS - 3
ER -