FMiTF: Track II: Alloy Analyzer Plus: An Integrated Development Environment for Alloy

FMiTF:轨道 II:合金分析仪 Plus:合金集成开发环境

基本信息

  • 批准号:
    2042871
  • 负责人:
  • 金额:
    $ 6.83万
  • 依托单位:
  • 依托单位国家:
    美国
  • 项目类别:
    Standard Grant
  • 财政年份:
    2020
  • 资助国家:
    美国
  • 起止时间:
    2020-07-15 至 2022-01-31
  • 项目状态:
    已结题

项目摘要

To deliver reliable and correct software systems, developers can create a software model, a representation of their software design written in a mathematical logic, which can then be checked for consistency. Unfortunately, the difficulty in writing models correctly remains a barrier to their adoption for large, complex software designs. This project develops the Alloy Analyzer Plus, an integrated development environment (IDE) toolset, that will provide a one-stop shop for software testing methods and enables the development of correct models written in the Alloy modeling language.Specifically, the project will create the Alloy Analyzer Plus IDE by building out two important infrastructure thrusts: first, the creation of workflows for verification techniques of Alloy models, enabling systematic unit testing, mutation testing and fault localization; and second, the creation of workflows for synthesis techniques of Alloy models, enabling correct from construction models through repair and sketching. These two thrusts will culminate in the creation of a guided development environment that can iteratively walk users through building correct models. This project bridges the gap between imperative IDEs and declarative-modeling IDEs. A robust verification-oriented IDE reduces the learning curve for Alloy and facilitates a larger adoption of software modeling. Furthermore, by enabling more reliable Alloy models, this project in turn leads to the development of more reliable software systems. The project will also help enhance formal methods curricula, as the Alloy Analyzer Plus synthesis capabilities provide an interactive tool to teach first-order logic. The project will extensively involve graduate students, notably those from underrepresented minorities, and expose them to formal methods and tool development.The main code base will be maintained for a minimum of three years on GitHub under the Apache License 2.0. The public repository, which will accumulate the code, documentation, and evaluation materials, is available at: [https://github.com/alloyanalyzerplus]. An associated GitHub Page will provide quick access to the latest stable release and tutorials for the extensions, and is available at: [https://alloyanalyzerplus.github.io].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 Plus,一个集成开发环境(IDE)工具集,将为软件测试方法提供一站式服务,并能够开发用Alloy建模语言编写的正确模型。具体来说,该项目将通过构建两个重要的基础设施来创建Alloy Analyzer Plus IDE:首先,创建Alloy模型验证技术的工作流程,实现系统化的单元测试、突变测试和故障定位;第二,创建Alloy模型合成技术的工作流程,通过修复和草图,实现从构造模型到正确。这两个目标最终将创建一个引导式开发环境,可以迭代地引导用户构建正确的模型。这个项目弥补了命令式IDE和声明式建模IDE之间的差距。一个健壮的面向验证的IDE缩短了Alloy的学习曲线,并促进了软件建模的广泛采用。此外,通过实现更可靠的Alloy模型,该项目反过来又导致了更可靠的软件系统的开发。该项目还将有助于加强正式的方法课程,因为合金分析仪加合成功能提供了一个交互式工具来教授一阶逻辑。该项目将广泛涉及研究生,特别是那些来自代表性不足的少数民族的研究生,并让他们接触正式的方法和工具开发。主要代码库将在Apache许可证2.0下在GitHub上维护至少三年。公共存储库将积累代码,文档和评估材料,可在[https://github.com/alloyanalyzerplus]上获得。相关的GitHub页面将提供对扩展的最新稳定版本和教程的快速访问,可在:[https://alloyanalyzerplus.github.io].该奖项反映了NSF的法定使命,并通过使用基金会的知识价值和更广泛的影响审查标准进行评估,被认为值得支持。

项目成果

期刊论文数量(3)
专著数量(0)
科研奖励数量(0)
会议论文数量(0)
专利数量(0)
Fault Localization for Declarative Models in Alloy
AlloyFL: a fault localization framework for Alloy
AlloyFL:Alloy 的故障定位框架
ProFL: a fault localization framework for Prolog
ProFL:Prolog 的故障定位框架
{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

数据更新时间:{{ journalArticles.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ monograph.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ sciAawards.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ conferencePapers.updateTime }}

{{ item.title }}
  • 作者:
    {{ item.author }}

数据更新时间:{{ patent.updateTime }}

Allison Sullivan其他文献

Evaluating State Modeling Techniques in Alloy
评估合金状态建模技术
  • DOI:
  • 发表时间:
    2017
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Allison Sullivan;Kaiyuan Wang;S. Khurshid;D. Marinov
  • 通讯作者:
    D. Marinov
Live Programming for Finite Model Finders
有限模型查找器的实时编程
LLM4TDD: Best Practices for Test Driven Development Using Large Language Models
LLM4TDD:使用大型语言模型进行测试驱动开发的最佳实践
  • DOI:
    10.48550/arxiv.2312.04687
  • 发表时间:
    2023
  • 期刊:
  • 影响因子:
    0
  • 作者:
    Sanyogita Piya;Allison Sullivan
  • 通讯作者:
    Allison Sullivan
Mutation testing for temporal alloy models (extended version)
  • DOI:
    10.1007/s10270-024-01220-x
  • 发表时间:
    2024-10-28
  • 期刊:
  • 影响因子:
    3.200
  • 作者:
    Ana Jovanovic;Allison Sullivan
  • 通讯作者:
    Allison Sullivan
Crucible: Graphical Test Cases for Alloy Models
Crucible:合金模型的图形测试用例

Allison Sullivan的其他文献

{{ item.title }}
{{ item.translation_title }}
  • DOI:
    {{ item.doi }}
  • 发表时间:
    {{ item.publish_year }}
  • 期刊:
  • 影响因子:
    {{ item.factor }}
  • 作者:
    {{ item.authors }}
  • 通讯作者:
    {{ item.author }}

{{ truncateString('Allison Sullivan', 18)}}的其他基金

CAREER: Live Programming for Finite Model Finders
职业:有限模型查找器的实时编程
  • 批准号:
    2337667
  • 财政年份:
    2024
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Continuing Grant
SHF: Small: INCA: Incremental Analysis of Software Specification for Evolving Systems
SHF:小型:INCA:不断发展的系统软件规范的增量分析
  • 批准号:
    2204536
  • 财政年份:
    2022
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant
FmitF: Track II: KeenEye: Enhancing Scenario Exploration
FmitF:轨道 II:KeenEye:增强场景探索
  • 批准号:
    2123341
  • 财政年份:
    2021
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant
FMiTF: Track II: Alloy Analyzer Plus: An Integrated Development Environment for Alloy
FMiTF:轨道 II:合金分析仪 Plus:合金集成开发环境
  • 批准号:
    1918189
  • 财政年份:
    2019
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant

相似海外基金

FMitF: Track II: Educating Developers about Ownership in Rust
FMITF:轨道 II:对开发人员进行 Rust 所有权教育
  • 批准号:
    2319014
  • 财政年份:
    2023
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant
FMitF: Track II: SMT-Based Reachability Analyzer of NGAC Policies
FMitF:轨道 II:NGAC 策略的基于 SMT 的可达性分析器
  • 批准号:
    2318891
  • 财政年份:
    2023
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track II: Cross-Language Support for Runtime Verification
合作研究:FMitF:轨道 II:运行时验证的跨语言支持
  • 批准号:
    2319473
  • 财政年份:
    2023
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant
FMitF: Track II: Bringing Verification-Aware Languages and Federated Authentication to Enable Secure Computing for Scientific Communities
FMITF:轨道 II:引入验证感知语言和联合身份验证,为科学界提供安全计算
  • 批准号:
    2319190
  • 财政年份:
    2023
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant
FMitF: Track II: Cybolic: a symbolic execution technique and tool for analyzing CMake build scripts
FMITF:轨道 II:Cybolic:用于分析 CMake 构建脚本的符号执行技术和工具
  • 批准号:
    2319131
  • 财政年份:
    2023
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track II: Cross-Language Support for Runtime Verification
合作研究:FMitF:轨道 II:运行时验证的跨语言支持
  • 批准号:
    2319472
  • 财政年份:
    2023
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track II: Enhancing the Neural Network Verification (NNV) Tool for Industrial Applications
合作研究:FMitF:轨道 II:增强工业应用的神经网络验证 (NNV) 工具
  • 批准号:
    2220418
  • 财政年份:
    2022
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant
Collaborative Research: FMitF: Track II: Enhancing the Neural Network Verification (NNV) Tool for Industrial Applications
合作研究:FMitF:轨道 II:增强工业应用的神经网络验证 (NNV) 工具
  • 批准号:
    2220426
  • 财政年份:
    2022
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant
FMitF: Track II: Usability, Scalability, and Deployment Improvement of VerioT
FMITF:轨道 II:VerioT 的可用性、可扩展性和部署改进
  • 批准号:
    2124225
  • 财政年份:
    2021
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant
FmitF: Track II: KeenEye: Enhancing Scenario Exploration
FmitF:轨道 II:KeenEye:增强场景探索
  • 批准号:
    2123341
  • 财政年份:
    2021
  • 资助金额:
    $ 6.83万
  • 项目类别:
    Standard Grant
{{ showInfoDetail.title }}

作者:{{ showInfoDetail.author }}

知道了