SHF: Small: Efficient Formal Analysis of Evolving Software Systems

University Of California-Irvine, Irvine CA

Investigators

Abstract

Modern software systems are very complex and tend to evolve over time. Formal specification languages and the corresponding analysis environments have shown promise in aiding the engineers to reason about the properties (e.g., security, reliability) of complex software systems. Despite their strengths, the reliance of such formally precise techniques on computationally heavy constraint solvers means that it can take a significant amount of time to verify the properties of software. This research devises a novel, and fully automated technique for efficient analysis of evolving software systems. The principles emerging from this research provide the foundation for making formal analysis of evolving software systems less expensive to conduct and more scalable, which in turn enable the vibrant software industry to significantly improve the quality of its products. The research produces a new breed of technologies with promising benefits for reduced defect density in specifications, designs, and code, achieved at reasonable cost, and within the constraints of real industrial settings. An opportunity to reduce the analysis time is presented by the fact that in a software development project, the formal specifications representing the software are unlikely to change completely from one analysis to the next. Unlike the existing analysis techniques that dispose of the prior results in response to changes in the system specification, the approach developed in this research automatically and efficiently updates the analysis results, where solutions to a prior system specification are leveraged to, among other things, narrow the space of values to be explored by the underlying constraint solver for the revised system specification, thereby greatly reducing the required computational effort. The intellectual merit of this research is a suite of optimization techniques to foster bounded verification of evolving software systems. The project advances the state-of-the-art by making bounded formal verification of software more scalable and cost effective, thereby expanding the domains in which such techniques can be applied.