Formal Verification of Hybrid Systems Using Global Optimization

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

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.