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.