SHF: Small: Tool Support for Verifiably-Robust Software

社会越来越依赖于软件的关键作用，崩溃可能会产生严重的后果，包括生命损失。例如，现在用软件来控制我们汽车的发动机和刹车是很常见的。 本研究探讨了一种新的方法来提高软件的弹性。 目标是验证隐藏的bug不会导致程序过渡到有问题的状态，在这种状态下，程序停止对人类控制做出响应，或者做出与测试时不同的响应。 鉴于我们的社会依赖于软件在关键角色的规模，提高软件弹性的新方法有可能减少软件故障的财务成本，甚至挽救生命。以前的工作主要集中在软件弹性的广泛测试或正式验证的正确性。 该项目采用了一种新的方法-它试图验证软件错误的后果在时间上是有限的。 准确地说，它验证在错误发生后的有限时间段后，执行将达到一种状态，在这种状态下，它将以测试时看到的相同行为进行响应。 这种特性在分布式系统文献中被称为自稳定。 该项目将联合收割机类型注释与编译器分析相结合，以验证计算是自稳定的。 该项目的第二个重点是探索如何将自稳定计算与有状态计算组合在一起，同时仍然提供有用的系统级保证。

Society increasingly relies on software in critical roles for which crashes can have serious consequences including the loss of lives. For example, it is now commonplace for software to control the engines and brakes in our cars. This research investigates a new approach for improving the resilience of software. The goal is to verify that hidden bugs cannot cause programs to transition into problematic states in which they stop responding to human control or respond differently than when they were tested. Given the scale that our society depends on software in critical roles, new approaches to improving software resilience have the potential to reduce the financial costs of software failures and even save lives.Previous work on software resilience largely focused on extensive testing or formal verification of correctness. This project takes a new approach - it seeks to verify that the consequences of a software error have a limited scope in time. Precisely, it verifies that after a bounded time period after an error, the execution will reach a state in which it will respond with same behaviors seen while testing. This property is known in the distributed systems literature as self-stabilization. The project will combine type annotations with compiler analyses to verify that a computation is self-stabilizing. A second thrust of the project is to explore how to compose self-stabilizing computations with stateful computations while still providing useful system level guarantees.