CAREER: Software Reliability via 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.