Pre-conference Workshop on Verification of Control Systems
From Home Page - Ufuk Topcu
|
Conference on Decision and Control (December 14, 2010)
Organizers: Bruce Krogh (CMU), Ufuk Topcu (Caltech)
Presenters: Patrick Cousot (NYU), Emilio Frazzoli (MIT), Bruce Krogh, Richard M. Murray (Caltech), George J. Pappas (UPenn), Andre Platzer (CMU), Claire Tomlin (UC Berkeley), and Ufuk Topcu
Registration information is available at Conference Registration Site.
Workshop Slides (will be posted after the workshop) -- email utopcu@cds.caltech.edu for the passcode.
Description
Model-based development of control systems makes it possible to verify the correctness of designs using simulation and formal methods before the control system is implemented. With recent convergence of controls, computation, and communication, there is a need for unified theories and algorithms. Despite advances in verfication tools in respective areas, such unification is in its infancy. Moreover, rigorous verification for systems of current interest is a complicated task due to common difficulties including the interaction the software and the physical world, untraditional information flow, modeling/environmental uncertainties, and unavoidable explosion of computational complexity of the currently available tools (in both domains). This pre-conference workshop aims to introduce fundamental concepts that have been used in formal verification of continuous, discrete, and hybrid control systems, and present recent advances in the application of these methods to control systems. The connections between the underlying theory, accompanying computational tools, and illustrative applications will be emphasized. The morning session consists of tutorial-type presentations covering the foundations of formal verification of continuous, discrete, and hybrid systems and current tools with motivating examples. The afternoon session comprises 45-minute presentations on current research on the theory and application of formal verification methods for control systems in a variety of application domains.
Tentative Program
Morning: Tutorials (8am-11:45am)
Morning tutorials will include topics such as introduction to and role of formal verification, hybrid system modeling, logical specifications, basic model checking and theorem proving, optimization-based verification of continuous systems. The exact schedule will be announced before the workshop and slides will be posted before the workshop. Presenters: Bruce Krogh, Andre Platzer, and Ufuk Topcu.
Afternoon: Research presentations
| 1- 1:45pm | Richard Murray, “Receding Horizon Temporal Logic Planning” |
| 1:45- 2:30pm | Emilio Frazzoli, “Sampling-Based Motion Planning with Deterministic mu-Calculus Specifications” |
| 2:30 - 3:15pm | Patrick Cousot, "Verification of Control Systems by Abstract Interpretation" |
| 3:30 - 4:15pm | Claire Tomlin, “Reachability-Based Controller Synthesis for Switched Systems” |
| 4:15pm-5pm | George Pappas, “Robust Verification of Control Systems” |
| 5pm-5:30pm | Wrap up |
Abstracts of the Research Presentations
Workshop Slides (will be posted after the workshop)
Biographies of the Presenters
- Patrick Cousot
Professor of Computer Science
New York University
Inventor, with Radhia Cousot, of Abstract Interpretation. Abstract interpretation is a theory of sound approximation of mathematical structures, in particular those involved in the behavior of computer systems. It allows the systematic derivation of sound methods and algorithms for approximating undecidable or highly complex problems in various areas of computer science (semantics, verification and proof, model-checking, static analysis, program transformation and optimization, typing, software steganography, etc.). Its current main industrial application is on the safety and security of complex hardware and software computer systems.
- Emilio Frazzoli
Associate Professor of Aeronautics and Astronautics at the Laboratory for Information and Decision Systems
Massachusetts Institute of Technology
He is a senior member of the American Institute of Aeronautics and Astronautics and of the Institute for Electrical and Electronics Engineers, and received a NSF CAREER award in 2002. Dr. Frazzoli’s research interests are focused mainly in the area of planning and control for mobile cyber-physical systems with an emphasis on autonomous vehicles, mobile robotics, and transportation networks.
- Bruce Krogh
Professor of Electrical and Computer Engineering
Carnegie Mellon University
He was founding Editor-in-Chief of the IEEE Transactions on Control Systems Technology and is a Distinguished Member of the IEEE Control Systems Society and a Fellow of the IEEE. His current research interests include distributed information processing and control, hybrid dynamic systems, and synthesis and verification of embedded control systems.
- Richard M. Murray
Thomas E. and Doris Everhart Professor of Control and Dynamical Systems and Bioengineering
California Institute of Technology
His research is in the application of feedback and control to networked systems, with applications in biology and autonomy. Current projects include verification and validation of distributed embedded systems, analysis of insect flight control systems, and biological circuit design.
- George J. Pappas
Joseph Moore Professor in the Department of Electrical and Systems Engineering
University of Pennsylvania
He also holds a secondary appointment in the Departments of Computer and Information Sciences, and Mechanical Engineering and Applied Mechanics, and is member and former director of the GRASP lab. He currently serves as the Deputy Dean in the School of Engineering and Applied Science. His research focuses on control theory and in particular, hybrid systems, embedded systems, hierarchical and distributed control systems, with applications to unmanned aerial vehicles, flight management systems, distributed robotics, and biomolecular networks. He is a Fellow of IEEE and has received various awards such as the George S. Axelby Award, and the National Science Foundation PECASE.
- Andre Platzer
Assistant Professor of Computer Science
Carnegie Mellon University
His research interests include hybrid systems, logic, automated theorem proving, model checking, symbolic and numerical computation. He introduced compositional verification techniques and methods that can verify hybrid systems without solving their differential equations (differential invariants). In addition, he led the development of the first theorem prover for hybrid systems (KeYmaera) and he has worked on verification of aircraft and train control systems.
- Claire Tomlin
Professor of Electrical Engineering and Computer Sciences
University of California, Berkeley
Research in hybrid systems, air traffic control automation, algorithms for decentralized optimization, modeling and analysis of biological cell networks.
- Ufuk Topcu
Postdoctoral Scholar in Control and Dynamical Systems
California Institute of Technology
His research, broadly speaking, focuses on the question how we can build robust and sustainable functional systems. To this end, he develops analytical and computational tools that aim to systematically and automatically close the specification-design-verification loop for dynamical systems. He received the Ph.D. in 2008 from the University of California, Berkeley.
Registration Information
Registration information is available at Conference Registration Site.
