Formal Verification of Hybrid Systems Using Global Optimization

题目：使用全局优化的混合系统的形式化验证基于逻辑的控制器嵌入在现代技术系统中，如汽车，航空和航天器，炼油厂和化学过程，发电厂和配电网络等，无处不在。这种系统的特点是连续状态动力学和基于逻辑控制器的离散状态动力学之间的耦合，同时负责联锁，排序和安全功能。随着对技术系统的性能和安全要求的增加，同时包含所有这些功能的基于逻辑的控制器的设计越来越复杂。一旦提出了设计，就非常需要正式地验证该设计确实实现了所有期望的功能。理想情况下，这一核查步骤应考虑到基础技术系统的持续动态。该项目正在开发能够适应这种混合系统的正式验证技术。混合系统的形式验证问题原则上可以用混合整数优化问题来表述和求解。然而，为了形式化验证的目的，必须保证在有限次数的迭代中找到优化问题的全局解。该项目正在为连续时域的混合系统开发新的确定性全局优化算法，可以提供这样的保证。

Proposal Number: 0208956Title: Formal Verification of Hybrid Systems Using Global OptimizationThe embedding of logic-based controllers in modern technological systems such as automobiles, air and spacecraft, oil refineries and chemical processes, power generation plants and distribution networks, etc., is ubiquitous. Such systems are characterized by a coupling between continuous state dynamics and the discrete state dynamics of the logic based controllers, which are simultaneously responsible for interlock, sequencing and safety functionality. As performance and safety demands on technological systems increase, the design of logic based controllers encompassing all these functionalities simultaneously is increasingly complex. Once a design has been proposed, it is highly desirable to verify formally that the design does indeed implement all the desired functionalities. Ideally this verification step should take into account the continuous dynamics of the underlying technological system. This project is developing formal verification technologies that can accommodate such hybrid systems.Formal verification problems for hybrid systems can in principle be formulated and solved as mixed-integer optimization problems. However, for formal verification purposes, it is essential to guarantee that the global solution of the optimization problem is found in a finite number of iterations. This project is developing novel deterministic global optimization algorithms for hybrid systems in the continuous time domain that can provide such guarantees.