Principal Investigator Paul Barton
The 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 strong coupling between continuous state dynamics of the underlying technological system 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 that the design does indeed implement all the desired functionalities in all possible situations. 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 discrete/continuous dynamic systems.
Formal verification problems for hybrid dynamic systems can in principle be formulated and solved as mixed-integer optimization problems (i.e., optimization problems involving both integer valued and real valued decision variables). However, for formal verification purposes, it is essential to guarantee that the global optimal solution of the optimization problem is found in a finite number of iterations; otherwise, the lack of a counterexample does not prove that a counterexample does not exist. This project is developing deterministic global optimization algorithms for hybrid dynamic systems in the continuous time domain that can provide such guarantees.