WHAT'S REAL IN 'REAL-TIME CONTROL SYSTEMS'? Applying formal verification methods and real-time rule-based systems to control systems and robotics

摘要

Engineers focus on the dynamics of control systems and robotics, addressing issues such as controllability, safety, and stability. To facilitate the control of increasingly complex physical systems such as drive-by-wire automobiles and fly-by-wire airplanes, high-performance networked computer systems with numerous hardware and software components are increasingly required. However, this complexity also leads to more potential errors and faults, during both the design/implementation phase and the deployment/runtime phase. It is therefore essential to manage the control system's complexity with the help of smart information systems and to increase its reliability with the aid of mechanical verification tools. Software control programs provide greater flexibility, higher precision, and better complexity management. However, these safety-critical real-time software must themselves be formally analyzed and verified to meet logical and timing correctness specifications. This keynote explores the use of rule-based systems in control systems and robotics, and describes the latest computer-aided verification tools for checking their correctness and safety.