Documentation for safety critical software

The authors review some of the fundamental difficulties presented by the design and the validation of software for safety critical applications. They suggest that software formal documentation techniques ameliorate the problems described. The principles behind a method of documenting both requirements and software design are presented. The methods have been used by the Atomic Energy Control Board of Canada in its safety assessment of the shutdown software of the Darlington generating station (D.L. Parnas et al., 1991). The method is illustrated by applying it to a small portion of the safety feature actuation system of a PWR nuclear reactor