Issue No. 01 - January/February (1994 vol. 11)
pp: 30-39, 28
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/52.251201
<p>Darlington is a four-reactor nuclear plant east of Toronto. It is operated by Ontario Hydro. Each reactor has two independent shutdown systems: SDS1 drops neutron-absorbing rods into the core, while SDS2 injects liquid poison into the moderator. Both are safety-critical and require high levels of confidence. In 1982, Ontario Hydro, with the concurrence of the Atomic Energy Control Board of Canada (AECB), had decided to fully implement the shutdown systems' decision-making logic on computers. This was to be the first Canadian instance of such a system, so there were questions about what procedures to follow, both in developing and licensing the system. To help achieve certification for the plant's shutdown systems, formal methods were applied to convince the AECB that the code was of acceptable quality and in accordance with specifications. Formal methods, applied only when serious concerns about the adequacy of the software and documentation arose, took the form of a formal model-based inspection.</p>
fission reactor core control and monitoring; fission reactor safety; nuclear engineering computing; formal specification; safety; software reliability; case study; Darlington nuclear generating station; nuclear plant; Ontario Hydro; software driven shutdown systems; neutron-absorbing rods; liquid poison injection; safety-critical systems; Atomic Energy Control Board of Canada; decision-making logic; Canada; licensing; certification; formal methods; code quality; specifications; documentation; formal model-based inspection
D. Craigen, S. Gerhart and T. Ralston, "Case Study: Darlington Nuclear Generating Station," in IEEE Software, vol. 11, no. , pp. 30-39, 28, 1994.