HAZARDS, DANGER CONDITION AND BASIC SAFETY POSTULATE IN ANALYSIS OF SAFETY-CRITICAL ALGORITHMS

摘要

The paper demonstrates a new way to development of clear and rigorous safety specifications for algorithms of safety-critical software. The proposed approach based upon the concepts and notions of Formal Qualitative Safety Analysis (FQSA). A given algorithm is described by Gurevich's Abstract State Machine. The analysis based upon the assumption that some Catastrophe Condition is specified. The analysis results in formal expressions for corresponding Catastrophe Inevitability Condition, Danger Condition, Safety Condition and Basic Safety Postulate for a given algorithm. Basic Safety Postulate establishes safety requirements for environment of a given algorithm and also characterizes the own internal safety of the algorithm by a qualitative logical way. Safety Condition allows making a safe version of the initial algorithm. All concepts and notions are introduced and illustrated during the analysis of simple inertial algorithm.