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.

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