FmitF: Track II: KeenEye: Enhancing Scenario Exploration

FmitF：轨道 II：KeenEye：增强场景探索

• 批准号: 2123341
• 负责人: Allison Sullivan
• 金额: $ 9.91万
• 依托单位: University of Texas at Arlington
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-10-01 至 2023-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2123341&HistoricalAwards=false
• 关键词: FmitF; Track; II; KeenEye; Enhancing

Scenario-finding toolsets are used to help computer scientists explore the correctness of their software by generating different examples of behavior allowed by the software system. Then, a user inspects these scenarios and makes sure the behavior matches their expectation. Since this inspection process is often done manually, scenario-finding tool sets should produce the fewest unique scenarios without missing important behavior. This project focuses on improvements to the scenario-finding toolset of the Alloy Analyzer. The project’s novelties are two-fold. First, this project integrates different enumeration strategies in the Alloy Analyzer to generate a more succinct collection of valuable scenarios. Second, this project improves the visual display of these scenarios so that computer scientists can more easily assess them for correct behavior. The project’s impacts are seen in the improved productivity of Alloy users who will no longer need to invest an intensive amount of time to build confidence in the correctness of their system.This project enhances the Alloy Analyzer’s enumeration engine in three ways. First, this project integrates Seabs, an abstract functions-based enumeration strategy, into the Alloy Analyzer and helps ease the adoption of Seabs by developing meta-templates for common types of abstract functions. Second, this project develops a novel enumeration strategy that allows the user to provide interactive guidance. Lastly, this project integrates several open-source enumeration strategies into the Analyzer, giving the user one consolidated toolset to fine-tune enumeration and target relevant scenarios. Moreover, this project improves the visualization of Alloy’s scenarios by generating views that declutter scenarios that span multiple system states and adding an annotated abstract syntax tree to visualize how logical constraints resolve to concrete values over the current scenario.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.

场景发现工具集用于帮助计算机科学家通过生成软件系统允许的不同行为示例来探索其软件的正确性。然后，用户检查这些场景，并确保行为符合他们的期望。由于此检查过程通常是手动完成的，因此，异常查找工具集应该在不遗漏重要行为的情况下产生最少的独特场景。这个项目的重点是改进合金分析仪的合金查找工具集。该项目的新颖之处有两个方面。首先，该项目在Alloy Analyzer中集成了不同的枚举策略，以生成更简洁的有价值场景集合。其次，该项目改进了这些场景的视觉显示，以便计算机科学家可以更容易地评估它们的正确行为。该项目的影响体现在Alloy用户的生产力提高上，他们将不再需要投入大量的时间来建立对系统正确性的信心。该项目从三个方面增强了Alloy Analyzer的枚举引擎。首先，该项目将Seabs（一种基于抽象函数的枚举策略）集成到Alloy Analyzer中，并通过为常见类型的抽象函数开发元模板来帮助简化Seabs的采用。第二，这个项目开发了一种新的枚举策略，允许用户提供交互式指导。最后，该项目将几个开源枚举策略集成到分析器中，为用户提供一个统一的工具集来微调枚举和目标相关场景。此外，该项目通过生成视图来简化跨越多个系统状态的场景，并添加带注释的抽象语法树来可视化逻辑约束如何在当前场景中解析为具体值，从而提高了Alloy场景的可视化效果。该奖项反映了NSF的法定使命，并通过使用基金会的智力价值和更广泛的影响评审标准进行评估，被认为值得支持。

项目成果

HawkEye: User-Guided Enumeration of Scenarios

HawkEye：用户引导的场景枚举

• DOI: 10.1109/issre52982.2021.00064
• 发表时间: 2021
• 期刊: 32nd IEEE International Symposium on Software Reliability Engineering
• 作者: Sullivan, Allison

Abstract Alloy Instances

抽象合金实例

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

REACH: Refining Alloy Scenarios by Size (Tools and Artifact Track)

REACH：按尺寸精炼合金场景（工具和神器轨道）

• DOI: 10.1109/issre55969.2022.00031
• 发表时间: 2022
• 期刊: The 33rd International Symposium on Software Reliability Engineering
• 作者: Jovanovic, Ana;Sullivan, Allison
• 通讯作者: Sullivan, Allison

Towards Automated Input Generation for Sketching Alloy Models

迈向绘制合金模型的自动输入生成

• DOI: 10.1145/3524482.3527651
• 发表时间: 2022
• 期刊: 10th IEEE/ACM International Conference on Formal Methods in Software Engineering
• 作者: Jovanovic, Ana;Sullivan, Allison
• 通讯作者: Sullivan, Allison