CAREER: Software Reliability via Assert-Generated Interfaces

构建可靠的软件系统仍然是一个具有挑战性的问题。主要的困难在于，这样的系统是通过集成由独立工作的开发人员编写的较小组件来构建的。每个组件只有在开发过程中尚未明确的某些特定条件下才能正确运行，从而使检查不同部分兼容性的任务复杂化。本研究建议开发断言生成接口，这是一个通过确保大型系统由兼容组件构建来提高软件可靠性的工具包。然后，各个组件构建器使用嵌入在实现中的断言语句在本地指定对组件正确工作至关重要的属性。这些断言将被自动分析，以获得描述如何安全地使用组件的接口。自动生成确保接口随着实现而发展。Assert Generated Interfaces将系统级正确性检查的任务分解为可管理的组件级检查，当无法进行静态检查时，可以使用这些接口构建包装器，通过阻止不安全的使用来动态地保护组件。

Building reliable software systems remains a challenging problem. The main difficulty is that such systems are built by integrating smaller components written by developers working in isolation. Each component functions correctly only under some specific conditions that remain unarticulated in the development process, thereby complicating the task of checking the compatibility of the different parts.This research proposes to develop Assert-Generated Interfaces, a toolkit to increase the reliability of software by ensuring that large systems are built from compatible components. Individual component builders then locally specify properties critical to the correct working of the components using assert statements embedded within the implementation. These assertions are automatically analyzed to obtain interfaces that describe how the component may be safely used. Automatic generation ensures the interface evolves with the implementation. Assert Generated Interfaces decompose the task of system-level correctness checking into manageable component-level checks, and when static checking is impossible, the interfaces can be used to build wrappers that dynamically shield components by blocking unsafe uses.