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

为了交付可靠和正确的软件系统，开发人员可以创建一个软件模型，即用数学逻辑编写的软件设计的表示，然后可以检查其一致性。不幸的是，正确编写模型的困难仍然是大型复杂软件设计采用模型的障碍。该项目开发了Alloy Analyzer Plus，这是一个集成开发环境（IDE）工具集，它将为软件测试方法提供一站式服务，并能够开发用Alloy建模语言编写的正确模型。具体来说，该项目将通过构建两个重要的基础设施来创建Alloy Analyzer Plus IDE：首先，创建Alloy模型验证技术的工作流程，实现系统单元测试、突变测试和故障定位；第二，合金模型合成技术的工作流程的创建，使正确的从建筑模型通过修复和草图。这两个重点将在引导开发环境的创建中达到高潮，该环境可以迭代地引导用户构建正确的模型。这个项目弥合了命令式ide和声明式建模ide之间的鸿沟。一个健壮的面向验证的IDE减少了Alloy的学习曲线，并促进了软件建模的广泛采用。此外，通过启用更可靠的Alloy模型，该项目反过来导致更可靠的软件系统的开发。该项目还将有助于加强形式方法课程，因为Alloy Analyzer Plus的合成功能提供了一个交互式工具来教授一阶逻辑。该项目将广泛涉及研究生，特别是那些来自代表性不足的少数民族的研究生，并使他们接触正式的方法和工具开发。主代码库将在Apache许可证2.0下在GitHub上维护至少三年。公共存储库将积累代码、文档和评估材料，可在以下地址获得：[https://github.com/alloyanalyzerplus]]。相关的GitHub页面将提供对最新稳定版本和扩展教程的快速访问，并可在[https://alloyanalyzerplus.github.io]]获得。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

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.