CAREER: Software Reliability via Assert-Generated Interfaces

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

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.