Safety and reliability of real-time engineering systems using formal methods.

摘要

From aircraft navigation systems to medical devices, computerized systems are occupying an increasingly important role in society. With our involvement in intelligent structures, and aerospace and nuclear applications, engineers must also be concerned about the safety and the reliability of the systems we develop to control, sense, and monitor. Consider for example the high dependability and fault tolerance required for active structural control. Because these real-time systems operate without a human in the loop, the impact of errors can be particularly devastating: control system failure could excite the structure rather than dissipate vibration. The overall goals of this research are to examine the impact of safety and reliability issues in real-time, engineering systems, and to define a practical methodology, consisting of both predeployment validation and run-time support, that can be used to ensure safety and reliability. More specifically, this study focuses on safety and reliability for active structural control as an example of an engineering application of real-time systems, and draws on notions such as formal modeling, formal verification, and real-time testing techniques to ensure correctness, as well as fault tolerance and redundancy to provide dependable behavior in the presence of hardware and software errors. The benefits of this study will enable the development of safe and reliable, fault-tolerant, real-time systems for practical engineering applications.