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

University Of Texas At Arlington, Arlington TX

Investigators

Abstract

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.