Safety validation of embedded control software using Z animation

Describes a rigorous approach to safety validation of embedded control software by specification animation. The software control logic is specified in Z and systematically animated together with a model of the equipment under control. All reachable equipment states under software control are systematically identified and compared with known hazardous states in normal operation and under dominant failure conditions. The process is completely automated, removing the need for human intervention and associated errors, and can be applied much earlier than traditional test-based techniques. As a result, the validation method has the potential to provide cost-effective, high-integrity safety assurance for embedded software. The approach is illustrated with a hypothetical industrial press control system.