SHF: Small: Efficient Formal Analysis of Evolving Software Systems

现代软件系统非常复杂，而且往往会随着时间的推移而发展。形式规范语言和相应的分析环境在帮助工程师对复杂软件系统的属性(例如，安全性、可靠性)进行推理方面显示出了良好的前景。尽管它们具有优势，但这种形式上精确的技术依赖于计算繁重的约束解算器，这意味着可能需要大量的时间来验证软件的属性。这项研究设计了一种新颖的、完全自动化的技术，用于有效地分析不断演变的软件系统。从这项研究中产生的原则为使对不断发展的软件系统进行正式分析的成本更低、可伸缩性更强提供了基础，这反过来又使充满活力的软件行业能够显著提高其产品质量。这项研究产生了一种新的技术，在实际工业环境的约束下，以合理的成本实现了降低规范、设计和代码中的缺陷密度的前景光明的好处。在软件开发项目中，表示软件的正式规范不太可能从一个分析到下一个完全改变，这为减少分析时间提供了机会。与响应于系统规范中的变化而处置先前结果的现有分析技术不同，本研究中开发的方法自动且高效地更新分析结果，其中利用先前系统规范的解决方案来缩小要由基础约束求解器为修订的系统规范探索的值空间，从而极大地减少所需的计算工作量。这项研究的智力价值是一套优化技术，以促进对不断发展的软件系统的有界验证。该项目通过使软件的有界形式验证更具可伸缩性和成本效益来推进最先进的技术，从而扩大了此类技术的应用领域。

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.