Verifying engineering systems using satisfiability modulo theories

计算算法和计算机硬件的进步使使用形式化技术测试网络**物理系统模型成为可能。在过去，这在计算上一直很难处理。对于一些与工业相关的工程模型，我们现在可以证明模型满足规定的要求。然而，要使足够大的一组模型实现这一点，**还有很多工作要做，以便这些技术和工具**将被业界采用。这个项目将通过专注于一组目前难以解决的**模型和需求来解决其中一些问题。如果没有进一步的洞察，根本的数学问题就不能足够快地解决，或者根本不能解决。该项目中提出的工作将有助于推进形式化方法测试的**最先进水平。今天正在研究和制作原型的网络物理系统在不久的将来将对社会产生巨大的影响。自动驾驶汽车和其他车辆、智能建筑、智能电网和个人生理监测都将改变我们生活的核心方面。但它们带来的最大挑战之一是如何确保它们的安全，我们**建议提供工具来测试和验证这些系统。行业合作伙伴是Quantum Research**Analytics(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.