Flashix II: Incremental verification of non-local refinements

Flashix项目的目标是对闪存文件系统进行全面验证。闪存现在是移动的和嵌入式系统的主导技术。它比传统存储器更快，更节能，更抗震。然而，其有效使用和寿命高度依赖于复杂的存储管理算法，这对最先进的验证技术提出了挑战。Flashix项目的第一阶段表明，在细化层次结构的背景下，已知的和新的技术可以用来解决这一挑战。然而，对系统崩溃，并发和非本地性能优化的鲁棒性达到了细化层次结构的模块化验证的实际限制。因此，在后续的项目中，我们开发了一个扩展，以促进模块化和增量验证的非局部细化的分层系统，它可以克服这些限制。这些问题不仅限于闪存文件系统，而且可以在许多嵌入式和性能关键型系统中找到。将新的验证技术应用到Flashix文件系统中，完成了其验证。其结果是一个经过充分验证的闪存文件系统，它在C中有效地实现了POSIX标准，并且可以在实践中部署。

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.