Documentation for safety critical software

The paper reviews some of the fundamental difficulties presented by the design and the validation of software for safety critical applications. It suggests 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, based on concepts proposed by H. D. Mills, D. L. Parnas, and J. Madey, have been used by the Atomic Energy Control Board of Canada in its safety assessment of the shutdown software of the Darlington generating station. The method is illustrated by applying it to a small portion of the safety feature actuation system of a PWR reactor.