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.

为了提供可靠和正确的软件系统，开发人员可以创建软件模型，这是其用数学逻辑编写的软件设计的表示，然后可以检查其一致性。不幸的是，正确编写模型的困难仍然是其采用大型，复杂软件设计的障碍。 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故障定位；其次，创建合成模型合成技术的工作流程，从构造模型中正确地通过修理和素描才能正确。这两个推力将在创建指导开发环境中达到顶峰，该环境可以迭代地通过构建正确的模型来延续用户。该项目弥合了当务之急和声明性模型IDE之间的差距。以良好的验证为导向的IDE减少了合金的学习曲线，并促进了更大的软件建模采用。此外，通过启用更可靠的合金模型，该项目又导致了更可靠的软件系统的开发。该项目还将有助于增强正式方法课程，因为Alloy Analyzer Plus合成功能提供了一种交互式工具来教授一阶逻辑。该项目将广泛涉及研究生，尤其是来自代表性不足的少数民族的研究生，并将其暴露于正式的方法和工具开发中。根据Apache许可证2.0，将在Github上至少维持三年的主要代码基础。公共存储库将累积代码，文档和评估材料，可在以下网址提供：[https：//github.com/alloyanalyalezerplus]。相关的GITHUB页面将快速访问扩展程序的最新稳定版本和教程，并在以下网址提供：[https：//alloyanalyerplus.github.io]。这一奖项反映了NSF的法定任务，并被认为是通过该基金会的知识分子的优点和广泛的影响来审查CRERIA的评估。

项目成果

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