IFAC 2014 Plenary Talk: Specification, Verification and Synthesis for Networked Control Systems
Abstract: Design of modern control systems involves the analysis and synthesis of feedback controllers at multiple levels of abstraction, from fast feedback loops around actuators and subsystems, to higher level decision-making logic in supervisory controllers and autonomous systems. One of the major challenges in design of complex networked control systems -- such as those arising in aerospace, computing, robotics, critical infrastructure and manufacturing systems, to name a few -- is insuring that the combination of dynamical behavior and logical decision-making satisfy detailed safety and performance specifications. In many of these areas, verification and validation are now dominant drivers of schedule and cost, and the tools available for design of such systems are falling behind the needs of systems and control engineers, particularly in the area of systematic design of the mixed continuous and discrete control laws for networked systems.
This talk focuses on work over the last 10 years by a variety of groups interested in rigorous specification and systematic synthesis of decision-making logic for hybrid systems. This decision-making logic is responsible for selecting modes of operation for the underlying (continuous) control system, reacting to external events and failures in the system, and insuring that the overall control system is satisfying safety and performance specifications. Tools from computer science, such as model-checking and logic synthesis, provide new approaches to solving these problems. A major shift is the move from "design then verify" to "specify then synthesize" approaches to controller design that allow simultaneous synthesis of high-performance, robust control laws and correct-by-construction decision-making logic. This talk will provide an overview of the relevant theory and recent results in this area, as well as include examples of their application to autonomous vehicles and aircraft electrical power distribution systems.
- Slides (PDF, 3.5MB)
- Videos of Alice the truck (from early testing)
- EECI short course (lectures, notes, references)
References
Some good references for the material that was presented:
Principles of Model Checking, C. Baier and J.-P. Katoen, The MIT Press, 2008.
Synthesis of Control Protocols for Autonomous Systems, N. Wongpiromsarn, U. Topcu and R. M. Murray. Unmanned Systems, 2013.
Additional references for individual topics are included on the lecture pages for the EECI short course.
