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.