Note: This content is accessible to all versions of every browser. However, this browser does not seem to support current Web standards, preventing the display of our site's design details.

  

Formal Verification Using Convex Optimization

Back
Abstract:
The complexity of modern engineering systems introduces the need to formally verify their correctness. Due to the infinite number of possibilities taken by the state and the uncertainties in these systems, exhaustive simulation is impossible, and also computing the set of reachable states is generally intractable. Nevertheless, the ever-increasing presence of such systems in safety critical applications makes it evident that verification is an issue that has to be addressed. In this talk, we will present a unified framework for verifying that a discrete, continuous, or hybrid system satisfies temporal specifications such as safety, reachability, eventuality, and their combinations. Our method does not require explicit computation of reachable states. Instead, functions of state termed barrier certificates and density functions are used in conjunction with deductive inference to prove properties of interest. As a consequence, the method is directly applicable to systems with nonlinearity, uncertainty, time-delay, and even stochasticity. We formulate verification using barrier certificates and density functions as convex optimization problems. For systems with polynomial descriptions, sum of squares programming can be used to construct polynomial barrier certificates and density functions in a computationally scalable manner. In addition, the convexity of the problem formulation can be exploited to prove a converse theorem in safety verification using barrier certificates. Some applications of the proposed method in other domains will also be outlined.

Type of Seminar:
Symposium on Control and Computation
Speaker:
Dr. Stephen Prajna
Caltech, USA
Date/Time:
Jun 22, 2005   16:15
Location:

ETH-Zentrum, Gloriastrasse 35, Zurich , Room ETZ E6
Contact Person:

Prof. M. Morari
No downloadable files available.
Biographical Sketch:
Stephen Prajna is currently a postdoctoral scholar at the California Institute of Technology (USA). He received the B.Eng. degree in Electrical Engineering from the Bandung Institute of Technology (Indonesia) in 1998, the M.S. degree in Mathematica Sciences from the University of Twente (The Netherlands) in 2000, and the Ph.D. degree in Control and Dynamical Systems from the California Institute of Technology in 2005. He has held short term visiting positions at ETH Zurich, Lund Institute of Technology, and University of Pennsylvania, and was a finalist of the Best Student Paper competition at the 2004 IEEE Conference on Decision and Control. His research interests include the general area of systems and control, convex optimization, and formal methods from control and computer science perspectives.