I-Corps: Automatic Formal Program Transformation for Improving Software Quality

I-Corps：自动正式程序转换以提高软件质量

• 批准号: 1646559
• 负责人: Grigore Rosu
• 金额: $ 5万
• 依托单位: University of Illinois at Urbana-Champaign
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-09-15 至 2017-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1646559&HistoricalAwards=false
• 关键词: Corps; Automatic; Formal; Program; Transformation

This I-Corps project explores the potential of using formal program transformation for improving commercial software quality. The broader impact/commercial potential of this I-Corps project is the use of an automatic program transformation technology which can significantly improve developer productivity and software quality. The technology improves software quality by automating the detection and fixing of bugs and other software issues, freeing developers to focus on other areas thus increasing their productivity. Fault-fixes are crucial for avoiding software bugs and, more generally, for maintaining high software quality. The automatic fixing technology will allow developers to easily and consistently avoid entire classes of bugs and software quality problems. In the long term, widespread use of this automatic program transformation system may result in fewer bugs that threaten life and property.The current practice in software fault repair is to automate fixes through custom scripts written by hand. However, this is an error-prone exercise and requires a very large development effort. This team's approach is to automate the fixes by expressing them as formal program transformation rules. The formal rules are powerful, allowing complex fixes, and are expressed in the underlying programming language. Consequently, they are easy to comprehend by developers. The underlying technology is the K framework, which has been successful as a specification and verification infrastructure for several widely-used programming languages, including JavaScript, Java, and C. Recent results indicate the K framework can also be used successfully for automatic program transformation.

这个i-Corps项目探索了使用正式程序转换来提高商业软件质量的潜力。这个i-Corps项目的更广泛的影响/商业潜力是使用自动程序转换技术，该技术可以显著提高开发人员的生产力和软件质量。这项技术通过自动检测和修复错误和其他软件问题来提高软件质量，使开发人员可以自由地专注于其他领域，从而提高他们的生产率。故障修复对于避免软件错误，更广泛地说，对于保持高软件质量是至关重要的。自动修复技术将使开发人员能够轻松一致地避免整个类别的错误和软件质量问题。从长远来看，这种自动程序转换系统的广泛使用可能会减少威胁生命和财产的错误。目前软件故障修复的做法是通过手动编写的自定义脚本自动修复。然而，这是一个容易出错的练习，并且需要非常大的开发工作。该团队的方法是通过将修复表达为正式的程序转换规则来实现修复的自动化。形式规则功能强大，允许进行复杂的修复，并以底层编程语言表示。因此，它们很容易被开发人员理解。它的底层技术是K框架，它已经成功地作为几种广泛使用的编程语言的规范和验证基础设施，包括Java、Java和C。最近的结果表明，K框架也可以成功地用于自动程序转换。