Safety-critical design for secure systems: Safety critical programs require a comprehensive approach, that combines the use of specialized languages and tools, rigorously controlled testing, and the use of formal methods

摘要

Traditional definition of a safety-critical program is one in which human life depends on the correct operation of the program. If there is a bug in such a program, then death or serious injury can result. Typical examples are signaling systems on trains, avionics control systems, medical instrumentation, and space applications. Since the focus is on human safety, we apply requirements to such programs that essentially require that they be error free. That's a strong requirement, especially given the common wisdom that all large programs contain serious errors. But in our modern technological age we place our safety at the mercy of computer software programs every time we board a train or plane, or enter a hospital, or even drive a car. We simply have to ensure the reliability of such programs, and as we will see in this paper, it is in fact possible and practical to achieve the seemingly very difficult goal of writing essentially error-free completely reliable software.