SHF: Small: INCA: Incremental Analysis of Software Specification for Evolving Systems

SHF：小型：INCA：不断发展的系统软件规范的增量分析

• 批准号: 2204536
• 负责人: Allison Sullivan
• 金额: $ 48.99万
• 依托单位: University of Texas at Arlington
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2204536&HistoricalAwards=false
• 关键词: SHF; Small; INCA; Incremental; Analysis

From the cars we drive to online banking, society has become increasingly dependent on software systems. As a result, software reliability remains an important problem to solve. One way developers can improve software reliability is by using software models, which allow developers to define the behavior of their software in the form of mathematical logic. Once a software system is modeled, various tools exist that automatically analyze the model for any issues with the software’s design. Unfortunately, software systems are not static: software is constantly getting updated as new features are added or requirements change. As the system evolves, the software model also needs to be updated and re-analyzed. However, if the change to the model is small, this analysis can be largely redundant. This project looks to improve the efficiency of re-running different types of analysis over an updated model, which increases the feasibility for maintaining models of real world systems. The project involves preparing students for their careers by mentoring graduate students and connecting students to role models in the formal methods community, and the tools developed by the project will improve formal methods education. The project focuses on improving incremental analysis of Alloy models based on three ways users can interact with a model: writing a model, testing a model, and synthesizing a model. First, this project explores improvements to incremental analysis when writing Alloy models, which focuses on how to maximize reuse of past scenarios and how to minimize the new scenario exploration problem. This project investigates a suite of techniques that derive new reuse and exploration strategies based on what component of the model changed and seek to present the impact of the change to the user through disjoint categories of scenarios. Second, this project explores improvements to incremental analysis when testing Alloy models, which includes introducing regression testing to Alloy as well as leveraging first order logic to automatically generate high value tests that reason over the changed portion of the model. Third, this project explores improvements to incrementally synthesizing Alloy models by pausing the sketch to generate tests to refine the synthesis problem and by creating an incremental, parallel sketching environment. In addition to research papers, the project will produce open-source toolsets and benchmarks of incremental models.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

从我们驾驶的汽车到网上银行，社会已经变得越来越依赖软件系统。因此，软件可靠性仍然是一个需要解决的重要问题。开发人员可以提高软件可靠性的一种方法是使用软件模型，该模型允许开发人员以数理逻辑的形式定义其软件的行为。一旦对软件系统建模，就可以使用各种工具自动分析模型，以发现软件设计中的任何问题。不幸的是，软件系统并不是一成不变的：随着新功能的添加或需求的变化，软件也在不断更新。随着系统的发展，软件模型也需要更新和重新分析。然而，如果模型的变化很小，这种分析可能在很大程度上是多余的。该项目旨在提高在更新的模型上重新运行不同类型的分析的效率，从而增加维护真实世界系统的模型的可行性。该项目包括通过指导研究生并将学生与正式方法社区中的榜样联系起来，为学生的职业生涯做好准备，该项目开发的工具将改善正式方法教育。该项目基于用户可以与模型交互的三种方式，重点改进了对合金模型的增量分析：编写模型、测试模型和合成模型。首先，这个项目探索了在编写合金模型时对增量分析的改进，重点是如何最大限度地重用过去的场景，以及如何最小化新的场景探索问题。该项目研究了一套技术，这些技术基于模型的哪些组件发生了变化而派生出新的重用和探索策略，并试图通过互不相交的场景类别向用户呈现变化的影响。其次，该项目探索了在测试合金模型时对增量分析的改进，包括向合金引入回归测试，以及利用一阶逻辑自动生成高值测试，以对模型的更改部分进行推理。第三，通过暂停草图以生成测试以改进合成问题，以及通过创建增量、并行的草图环境，该项目探索了对增量合成合金模型的改进。除了研究论文，该项目还将产生增量模型的开源工具集和基准。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

Abstract Alloy Instances

抽象合金实例

• 发表时间: 2023
• 期刊: Formal Methods - 25th International Symposium
• 作者: Ringert, J.O.;Sullivan, A.
• 通讯作者: Sullivan, A.