Verifying engineering systems using satisfiability modulo theories

点击翻译按钮获取中文摘要

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.