SHF: Small: INCA: Incremental Analysis of Software Specification for Evolving Systems

点击翻译按钮获取中文摘要

From the cars we drive to online banking, society has become increasingly dependent on software systems. As a result, software reliability remains an important problem to solve. One way developers can improve software reliability is by using software models, which allow developers to define the behavior of their software in the form of mathematical logic. Once a software system is modeled, various tools exist that automatically analyze the model for any issues with the software’s design. Unfortunately, software systems are not static: software is constantly getting updated as new features are added or requirements change. As the system evolves, the software model also needs to be updated and re-analyzed. However, if the change to the model is small, this analysis can be largely redundant. This project looks to improve the efficiency of re-running different types of analysis over an updated model, which increases the feasibility for maintaining models of real world systems. The project involves preparing students for their careers by mentoring graduate students and connecting students to role models in the formal methods community, and the tools developed by the project will improve formal methods education. The project focuses on improving incremental analysis of Alloy models based on three ways users can interact with a model: writing a model, testing a model, and synthesizing a model. First, this project explores improvements to incremental analysis when writing Alloy models, which focuses on how to maximize reuse of past scenarios and how to minimize the new scenario exploration problem. This project investigates a suite of techniques that derive new reuse and exploration strategies based on what component of the model changed and seek to present the impact of the change to the user through disjoint categories of scenarios. Second, this project explores improvements to incremental analysis when testing Alloy models, which includes introducing regression testing to Alloy as well as leveraging first order logic to automatically generate high value tests that reason over the changed portion of the model. Third, this project explores improvements to incrementally synthesizing Alloy models by pausing the sketch to generate tests to refine the synthesis problem and by creating an incremental, parallel sketching environment. In addition to research papers, the project will produce open-source toolsets and benchmarks of incremental models.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.