Comprehensive evaluation of file systems robustness with SPIN model checking. (20th July 2022)

• Record Type: Journal Article
• Authors: Yuan, Jingcheng; Aoki, Toshiaki; Guo, Xiaoyun
• Is Part Of: Software testing, verification & reliability. Volume 32:Number 6(2022)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2022-07-20
• Subjects: file system -- model checking -- power outage -- Promela -- robustness -- SPIN; Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1828
• Languages: English
• ISSNs: 0960-0833

Abstract

Summary: In existing computer systems, file systems are indispensable for organizing user data and system codes. However, several studies have reported certain file system errors that cause significant data loss or system crashes. Most of these errors are due to external failures, such as an unexpected power outage. However, comprehensively evaluating file system robustness to detect these errors is challenging. The various types of file systems use different data structures and algorithms for various applications. Moreover, file system errors may be triggered by an unpredictable external condition. In addition, a file system works in an operating system's kernel layer as a passive module and runs in a multi‐thread mode, which makes file system testing time‐intensive. Furthermore, the large number of states in file systems leads to greedy checking, which results in a state explosion. In this study, we comprehensively evaluated the robustness expected in multiple properties of file systems using a model checking approach. The evaluation covered the majority of the mainstream file system types and included both single‐thread and multi‐thread modes. We developed Promela models that abstracted the real file systems and subsequently checked them using a SPIN model checker. Our model was optimized to avoid state explosion during model checking. Using the model checking, we successfully detected corner‐case errors during an unexpected power outage. By analysing counterexamples generated by model checking, we determined an improved file system model capable of preventing errors in most mainstream file system types. Finally, we rechecked the improved file system model and verified the absence of all critical errors. Abstract : In this study, we comprehensively evaluated the robustness of the mainstream file system types, expected in multiple properties and both single‐thread and multi‐thread modes. We developed Promela models that abstracted the real file systems, optimized them to avoid state explosion, checked them using a SPIN model checker, and detected corner‐case errors in the condition of an unexpected power outage. By analysing counterexamples, we developed an improved file system model that verified the absence of all critical errors.