FmitF: Track II: KeenEye: Enhancing Scenario Exploration

点击翻译按钮获取中文摘要

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.