SHF: Small: Tool Support for Verifiably-Robust Software

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

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.