BROWSE
Detail
Conference Paper
Model-based Kernel Testing for Concurrency Bugs through Counter Example Replay
Cited - time in 
Share 
Share
- Authors
- Moon Zoo Kim, Shin Hong, Chang Ki Hong, Tae Ho Kim
- Issue Date
- 2009-03
- Citation
- Workshop on Model Based Testing (MBT) 2009, pp.21-36
- Language
- English
- Type
- Conference Paper
- Abstract
- Despite the growing need for customized operating system kernels for embedded devices, kernel development continues to suffer from high development and testing costs for several reasons, including the high complexity of the kernel code, the infeasibility of unit testing, exponential numbers of concurrent behaviors, and a lack of proper tool support. To alleviate these difficulties, this study proposes the MOdel-based KERnel Testing (MOKERT) framework, which supports detection of concurrency bugs in the kernel by combining both model checking techniques and testing methods. The MOKERT framework was applied to the file systems of the Linux 2.6 kernel and found a data race bug in the proc file system.
- KSP Keywords
- Data race, File System, Operating system kernel, Testing method, Tool support, Unit Testing, concurrency bugs, embedded device, model checking, model-based, need for