CAREER: Software Reliability via Assert-Generated Interfaces

职业：通过断言生成的接口实现软件可靠性

• 批准号: 0644361
• 负责人: Ranjit Jhala
• 金额: $ 40万
• 依托单位: University of California-San Diego
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2007
• 资助国家: 美国
• 起止时间: 2007-06-01 至 2013-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0644361&HistoricalAwards=false
• 关键词: CAREER; Software; Reliability; via; 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.

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