Verifying engineering systems using satisfiability modulo theories

使用可满足性模理论验证工程系统

• 批准号: 536684-2018
• 负责人: Ingalls, Colin
• 金额: $ 0.91万
• 依托单位: Carleton University
• 依托单位国家: 加拿大
• 项目类别: Engage Plus Grants Program
• 财政年份: 2018
• 资助国家: 加拿大
• 起止时间: 2018-01-01 至 2019-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=654269
• 关键词: Verifying; engineering; systems; using; satisfiability

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.

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