Title :
Safety validation of embedded control software using Z animation
Author :
Atchison, Brenton M. ; Lindsay, Peter A.
Author_Institution :
Queensland Univ., Brisbane, Qld., Australia
Abstract :
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
Keywords :
computer animation; computerised control; embedded systems; engineering graphics; industrial control; program verification; reachability analysis; safety-critical software; specification languages; state estimation; Z specification language; automated process; cost-effective high-integrity safety assurance; dominant failure conditions; embedded control software; equipment model; hazardous states; industrial press control system; reachable equipment state identification; safety validation; software control logic; specification animation; validation method; Animation; Automatic control; Automatic testing; Control systems; Electrical equipment industry; Embedded software; Humans; Logic; Software safety; Software systems;
Conference_Titel :
High Assurance Systems Engineering, 2000, Fifth IEEE International Symposim on. HASE 2000
Conference_Location :
Albuquerque, NM
Print_ISBN :
0-7695-0927-4
DOI :
10.1109/HASE.2000.895467
