Flashix II: Incremental verification of non-local refinements

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