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.


Verification and Synthesis of Hybrid Systems Using Proximity-Based Automata

Often, the correctness of embedded control system designs is verified using simulation and testing, which is time consuming and does not capture all possible system behaviors. Techniques proposed for performing formal verification for embedded systems are based on predicate abstractions, which are transition systems reflecting a partition of the state space of models called hybrid systems. Hybrid systems capture the dynamics of embedded control systems with discrete and continuous state variables. This talk focuses on an alternative technique for automatic verification of safety properties for hybrid systems based on the Proximity-Based Automaton (PBA), a finite-state representation of the infinite-state behaviors of the hybrid system. In contrast to predicate abstractions, PBAs can be constructed efficiently for systems that exhibit a significant amount of switching and have discrete input sets. The notion of proximity of states in the continuous-valued state space is used to construct PBAs using ellipsoidal techniques and tools for solving optimization problems constrained by linear matrix inequalities. The PBAs are also used to solve an input sequence synthesis problem by using the PBA structure to formulate an informed search problem, whose solution is guided by a dynamic programming estimate of the solution.

Type of Seminar:
Public Seminar
Dr. Jim Kapinski
Curtiss-Wright, Advanced Products and Systems Division
Nov 22, 2005   17:15

ETL K 25
Contact Person:

Dr. G. Papafotiou
File Download:

Request a copy of this publication.
Biographical Sketch:
Dr. James Kapinski received his B.S.E.E. from the University of Pittsburgh in 1996. From 1996 to 1998 he worked for AK Steel as an electrical engineer. He entered graduate school in 1998 and received his M.S.E.E. from the University of Pittsburgh in 1999. From 1999 to 2000 he worked for Westinghouse, Electromechanical Division, where his work focused on the modeling and control of electromagnetic launch systems. In 2000 he returned to graduate school and received his Ph.D. from Carnegie Mellon University in 2004. He is currently with Curtiss-Wright, Advanced Products and Systems Division developing pulsed power systems. His research interests include control theory, verification and synthesis for hybrid systems, and modeling and control of electric machines.