A safety-critical software design and verification technique

Safe software can be developed by applying a safety-oriented design method and establishing good safety management procedures. However, safety-oriented design has not received much research attention in the past.This dissertation proposes a software design method whose goal is to minimize the amount of safety-critical code and to produce a design whose safety can be verified. Starting from the software safety requirements, backward analysis is used to identify the safety-critical modules and derive their safety constraints. Safety constraints play an important role since they become the criteria against which the safety of detailed design is verified. This dissertation also proposes the use of information hiding principles to implement a "firewall." The firewall protects the safety-critical modules from the safety-independent modules, thereby minimizing the amount of safety verification effort required in formally certifying the design safety. The complexity of design safety verification is further reduced by employing an incremental and selective verification. This dissertation argues that concurrency decisions on safety-critical software must be based on careful trade-off analysis and demonstrates that concurrent designs do not necessarily require exhaustive concurrency safety verification. An application of the proposed safety-oriented design method is demonstrated using a subsystem of TCAS II (Traffic Alert and Collision Avoidance System).Management aspects of software safety are important because of the direct and significant impact management has on safety. This dissertation examines how to organize safety-critical projects and distribute safety responsibilities