FMitF: Track I: Automating the Verification of Distributed Systems

计算机软件现在是，而且一直是充满错误的。当这些错误在部署的系统中出现时，它们可能会导致严重的问题，包括不期望的行为和关键服务的不可用。形式验证是一种允许编写可证明没有此类错误的软件的方法，但众所周知，它非常困难和耗时，这使得它更难在实践中采用。该研究将探索一种新的方法来自动验证运行在多台机器上的复杂软件，从而使形式验证更接近成为现实。该建议将通过自动识别归纳不变量来自动化验证过程。它使用模型检查来识别系统的一个小的有限实例的归纳不变量，然后尝试将该不变量推广到所有可能的实例。拟议的工作是按照沿着三个要点安排的。第一个推力将扩大这个最初的想法，以涵盖存在量词的不变量，从而扩大了方法的范围。第二个重点是通过增加对细化的支持，将该方法扩展到更复杂的系统。第三个推力将超越可判定的验证，以支持高性能的实现。第一，它是使正式核查更接近实际用途并确保其不再仅仅是一种学术活动的途径。这将进一步促进构建和部署稳定可靠的系统，使所有最终用户立即受益。在学术方面，该项目旨在揭穿普遍认为模型检查不适用于复杂的分布式系统，由于其有限的可扩展性。通过这样做，这个项目将把定理证明和模型检查结合在一起，这两个领域长期以来一直在朝着正确性的方向并行前进。通过这项工作生成的数据（规范、实现、证明、配置和脚本文件）将保留在由主要研究者的研究小组管理的安全机器集群中，电子数据备份服务由密歇根州电气工程和计算机科学系的部门计算组织以及密歇根大学的信息和技术服务提供。它们也将托管在github.com等公开可用的存储库提供商上。根据NSF指南的要求，数据将在授予期后至少保留三年。当前的存储库可以在以下网站找到：https://github.com/GLaDOS-Michigan/I4.This奖项反映了NSF的法定使命，并被认为值得通过使用基金会的知识价值和更广泛的影响审查标准进行评估来支持。

Computer software is and has always been teeming with errors. When these errors manifest in a deployed system they can cause severe problems, including undesired behavior and unavailability of critical services. Formal verification is an approach that allows the writing of software that is provably free of such errors, but is notoriously difficult and time-consuming, which makes it harder to adopt in practice. The proposed research will investigate a new approach for automating the verification of complex software running on multiple machines, thus bringing formal verification closer to becoming a practical reality.This proposal will automate the verification process by automatically identifying inductive invariants. It uses model checking to identify an inductive invariant of a small, finite instance of the system and then tries to generalize that invariant to all possible instances. The proposed work is structured along three thrusts. The first thrust will expand this initial idea to cover invariants with existential quantifiers, thus broadening the scope of the approach. The second thrust will scale the approach to more complicated systems by adding support for refinement. The third thrust will go beyond decidable verification in order to support high-performance implementations.The proposed work’s broader impact is multi-faceted. First, it represents a path for bringing formal verification closer to practical use and ensuring it does not remain just an academic exercise. This will further enable building and deploying stable and reliable systems to the immediate benefit of all end users. On the academic side, this project aims to debunk the common belief that model checking is not applicable to complex distributed systems due to its limited scalability. By doing so, this project will bring together theorem proving and model checking, two areas that have long been walking parallel paths towards correctness. The data generated through this work (specifications, implementations, proofs, configurations and script files) will be retained in a secure machine cluster administered by the research groups of the principal investigators, with electronic data backup service provided by the Departmental Computing Organization of the Electrical Engineering and Computer Science Department at Michigan and the Information and Technology Services of the University of Michigan. They will also be hosted on publicly available repository providers like github.com. Data will be retained for at least three years beyond the award period, as required by NSF guidelines. The current repository can be found at: https://github.com/GLaDOS-Michigan/I4.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.