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.