Verifying engineering systems using satisfiability modulo theories

计算算法和计算机硬件的进步使得使用正式技术测试网络物理系统模型成为可能。这在过去一直是难以计算的。对于一些工业相关的工程模型，我们现在可以证明模型满足规定的需求。然而，**仍然有很多工作要做，以使足够大的模型集成为可能，以便技术**和工具将被行业采用。这个项目将通过关注当前难以处理的一组模型和需求来解决其中的一些问题。如果没有进一步的洞察力，根本不可能很快解决潜在的数学问题。在这个项目中提出的工作将有助于推动正式方法测试的最新技术。目前正在研究和制作原型的网络物理系统**将在不久的将来对社会产生巨大影响。自动驾驶汽车和其他交通工具、智能建筑、智能电网和个人生理监测都将改变我们生活的核心方面。但他们提出的最大挑战之一是如何确保他们的安全，我们建议提供测试和验证这些系统的工具。行业合作伙伴是量子研究**分析公司（QRA）。QRA对真实世界的系统进行正式测试。我们建议开发必要的数学和软件，以扩大QRA可以测试的系统范围。特别是，我们将**扩展可以使用QRA将提供的**实际行业问题中出现的可满足模理论来解决的数学理论的数量。研究生和本科生也将**参与本研究。我们将从目前**方法无法解决的实际行业问题开始，我们将通过在当前**解决方案中添加新的理论或数学来解决这些问题。这将产生一个具有扩展功能的新软件，可用于正式验证新系统。

Advances in computing algorithms and computer hardware have made it possible to test models of cyber**physical systems using formal techniques. This has been computationally intractable in the past. For some**industrially-relevant engineering models, we now can prove that a model meets stated requirements. However,**there is still much work to do to make this possible for a large enough set of models such that the techniques**and tools will be adopted by industry. This project will tackle some of those problems by focusing on a set of**models and requirements that are currently intractable. The underlying mathematical problems cannot be**solved quickly enough or at all without further insight. The work proposed in this project will help advance the**state-of-the-art in formal methods testing. The cyber physical systems that are being researched and prototyped**today will have a tremendous impact on society in the near future. Self-driving cars and other vehicles, smart**buildings, smart power grids, and personal physiological monitoring are all poised to change central aspects of**our lives. But one of the biggest challenges they present is how to ensure they are safe and secure, and we**propose to provide tools for testing and verifying these systems. The industry partner is Quantum Research**Analytics (QRA). QRA carries out formal testing of real world systems. We propose to develop the**mathematics and software necessary to expand the range of systems that QRA can test. In particular, we will**expand the number of mathematical theories that can be solved using satisfiablity modulo theories that occur in**actual industry problems that QRA will supply. Graduate students and undergraduate students will also**contribute to this research. We will begin by taking actual industry problems that can not be solved by current**methods, and we will work to solve these problems by adding new theories, or mathematics, to the current**solvers. This will yield an new software with expanded functionality that can be used to formally verify new**systems.