Pervasive formal verification in control system design

Control systems design is a multifaceted field, drawing not only on control theory, but on results from computer science, electrical engineering, mechanical engineering, and physics. A controller often must satisfy regimented size, weight, power, and timing constraints, integrate with the overall system, and perform properly in a variety of harsh environments. Furthermore, control systems are arguably the lynchpin of safety in critical embedded systems, ranging from nuclear reactors to avionics to medical devices. Progress has been made in the formal verification of aspects of control system design. Advances in hybrid system verification show promise in automating the verification of abstract models of dynamical systems. Advances in software and hardware formal verification may contribute to ensuring the correctness of implementations. Nevertheless, industrial uptake of these advances is still in its infancy, particularly as compared to disciplines such as digital hardware design. This panel will address the impediments to the adoption of formal verification techniques in industrial control system design. Furthermore, the panel will address what research topics would most benefit the adoption of formal verification in industry.