Flashix II: Incremental verification of non-local refinements

点击翻译按钮获取中文摘要

The aim of the Flashix project is the full-scale verification of a flash file system. Flash memory is by now the dominant technology for mobile and embedded systems. It is faster, more energy-efficient and shock-resistant than traditional memory. However, its efficient use and life span are highly dependent upon complex storage management algorithms, posing a challenge for state-of-the-art verification technology. The first phase of the Flashix project demonstrated that known and new techniques in the context of refinement hierarchies can be employed to tackle this challenge. However, robustness against system crashes, concurrency and non-local performance optimizations reach the practical limitations of a modular verification with refinement hierarchies. In the follow-up project we therefore develop an extension to facilitate a modular and incremental verification of non-local refinements in hierarchical systems, which can overcome these limitations. The problems are not limited to flash file systems, but can be found in many embedded and performance-critical systems. The new verification technique is applied to the Flashix file system, completing its verification. The result is a fully verified file system for flash memory that efficiently implements the POSIX standard in C and is deployable in practice.