SHF:Large:Collaborative Research: Inferring Software Specifications from Open Source Repositories by Leveraging Data and Collective Community Expertise

SHF：大型：协作研究：利用数据和集体社区专业知识从开源存储库推断软件规范

• 批准号: 1518776
• 负责人: Robert Dyer
• 金额: $ 21.48万
• 依托单位: Bowling Green State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2015
• 资助国家: 美国
• 起止时间: 2015-07-01 至 2019-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1518776&HistoricalAwards=false
• 关键词: SHF; Large; Collaborative; Research; Inferring

Today individuals, society, and the nation critically depend on software to manage critical infrastructures for power, banking and finance, air traffic control, telecommunication, transportation, national defense, and healthcare. Specifications are critical for communicating the intended behavior of software systems to software developers and users and to make it possible for automated tools to verify whether a given piece of software indeed behaves as intended. Safety critical applications have traditionally enjoyed the benefits of such specifications, but at a great cost. Because producing useful, non-trivial specifications from scratch is too hard, time consuming, and requires expertise that is not broadly available, such specifications are largely unavailable. The lack of specifications for core libraries and widely used frameworks makes specifying applications that use them even more difficult. The absence of precise, comprehensible, and efficiently verifiable specifications is a major hurdle to developing software systems that are reliable, secure, and easy to maintain and reuse. This project brings together an interdisciplinary team of researchers with complementary expertise in formal methods, software engineering, machine learning and big data analytics to develop automated or semi-automated methods for inferring the specifications from code. The resulting methods and tools combine analytics over large open source code repositories to augment and improve upon specifications by program analysis-based specification inference through synergistic advances across both these areas. The broader impacts of the project include: transformative advances in specification inference and synthesis, with the potential to dramatically reduce, the cost of developing and maintaining high assurance software; enhanced interdisciplinary expertise at the intersection of formal methods software engineering, and big data analytics; Contributions to research-based training of a cadre of scientists and engineers with expertise in high assurance software.

如今，个人，社会和国家非常依赖软件来管理关键的电力，银行和金融，空中交通管制，电信，运输，国防和医疗保健。规格对于将软件系统的预期行为传达给软件开发人员和用户至关重要，并使自动化工具可以验证给定软件是否确实按预期行为是可能的。传统上，安全关键应用程序享受了此类规格的好处，但付出了很大的代价。 因为从头开始生产有用的，非平凡的规格非常困难，耗时，并且需要不可广泛的专业知识，因此这些规格在很大程度上不可用。缺乏核心库和广泛使用框架的规格使指定使用它们更加困难的应用程序。缺乏精确，可理解和有效的可验证规格是开发可靠，安全且易于维护和重复使用的软件系统的主要障碍。该项目汇集了一个跨学科的研究人员团队，具有正式方法，软件工程，机器学习和大数据分析方面的互补专业知识，以开发自动化或半自动化方法，以从代码中推断规格。最终的方法和工具结合了大型开源代码存储库上的分析，以通过基于程序分析的规范推论来增强和改进规格，通过这两个领域的协同进步。该项目的更广泛影响包括：规范推断和综合方面的变革性进步，有可能大大减少开发和维持高保证软件的成本；在形式方法工程和大数据分析的交集中增强了跨学科专业知识；对具有高保证软件专业知识的科学家和工程师干部的基于研究的培训的贡献。