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.

为了交付可靠和正确的软件系统，开发人员可以创建软件模型，这是用数理逻辑编写的软件设计的表示，然后可以检查该模型的一致性。不幸的是，正确编写模型的困难仍然是大型复杂软件设计采用模型的障碍。该项目开发了一个集成开发环境(IDE)工具集，它将为软件测试方法提供一站式商店，并使以合金建模语言编写的正确模型的开发成为可能。具体地说，该项目将通过构建两个重要的基础设施来创建合金Analyzer Plus IDE：第一，为合金模型的验证技术创建工作流，实现系统的单元测试、突变测试和故障定位；第二，为合金模型的合成技术创建工作流，从构建模型到修复和绘制都是正确的。这两个目标将最终导致创建一个指导开发环境，该环境可以迭代地引导用户构建正确的模型。这个项目在命令式IDE和声明性建模IDE之间架起了桥梁。强大的面向验证的集成开发环境降低了合金的学习曲线，并促进了软件建模的更广泛采用。此外，通过启用更可靠的合金模型，该项目反过来又导致更可靠的软件系统的开发。该项目还将帮助加强正式的方法课程，因为合金分析器和合成能力提供了一个交互工具来教授一阶逻辑。该项目将广泛涉及研究生，特别是那些来自代表性不足的少数族裔的研究生，并让他们接触正式的方法和工具开发。主代码库将根据阿帕奇许可证2.0在GitHub上维护至少三年。公共存储库将积累代码、文档和评估材料，可在以下位置获得：[https://github.com/alloyanalyzerplus].相关的GitHub页面将提供对最新稳定版本和扩展教程的快速访问，并可在以下位置获得：[https://alloyanalyzerplus.github.io].This奖反映了美国国家科学基金会的法定使命，并已通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

项目成果

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

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

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