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

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

• 批准号: 1918189
• 负责人: Allison Sullivan
• 金额: $ 10万
• 依托单位: North Carolina Agricultural & Technical State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2019
• 资助国家: 美国
• 起止时间: 2019-08-01 至 2020-10-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1918189&HistoricalAwards=false
• 关键词: FMiTF; Track; II; Alloy; Analyzer

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 通过构建两个重要的基础设施主旨：第一，创建合金模型验证技术的工作流程，实现系统的单元测试、突变测试和故障定位；其次，为合金模型的合成技术创建工作流程，通过修复和绘制草图来实现从构造模型的正确性。这两个推动力最终将创建一个引导式开发环境，可以迭代地引导用户构建正确的模型。该项目弥补了命令式 IDE 和声明式建模 IDE 之间的差距。强大的、面向验证的 IDE 缩短了 Alloy 的学习曲线，并促进软件建模的更广泛采用。此外，通过实现更可靠的 Alloy 模型，该项目反过来又促进了更可靠的软件系统的开发。该项目还将有助于增强形式方法课程，因为合金分析仪加综合功能提供了一个交互式工具来教授一阶逻辑。该项目将广泛吸引研究生，特别是来自代表性不足的少数族裔的研究生，并使他们接触正式的方法和工具开发。主要代码库将根据 Apache License 2.0 在 GitHub 上维护至少三年。公共存储库将积累代码、文档和评估材料，可从以下位置获取：[https://github.com/alloyanalyzerplus]。相关的 GitHub 页面将提供对最新稳定版本和扩展教程的快速访问，可在以下位置获取：[https://alloyanalyzerplus.github.io]。该奖项反映了 NSF 的法定使命，并被认为值得通过以下方式获得支持：使用基金会的智力价值和更广泛的影响审查标准进行评估。

项目成果

Solution Enumeration Abstraction: A Modeling Idiom to Enhance a Lightweight Formal Method

解决方案枚举抽象：增强轻量级形式方法的建模习惯

• DOI: 10.1007/978-3-030-32409-4_21
• 发表时间: 2019-10
• 期刊: International Conference on Formal Engineering Methods
• 作者: Sullivan, Allison;Marinov, Darko;Khurshid, Sarfraz
• 通讯作者: Khurshid, Sarfraz