Application of Tabular Methods to the Speciflcation and Veriflcation of a Nuclear Reactor Shutdown System
Mark Lawford · 2001
This paper describes the use of tabular methods at Ontario Power Generation Inc. (OPGI) 1 on the Darlington Nuclear Generating Station Shutdown System (SDS) Trip Computer Software Redesign Project. We flrst motivate the selection of tabular methods and provide an overview of the Systematic Design Veriflcation (SDV) procedure. After reviewing some preliminary concepts, the paper describes how the Software Engineering Standards and Methods (SESM) Tool suite is used with SRI's automated proof assistant, PVS, to provide tool support for the use of tabular methods in the software engineering process. Examples based upon the Systematic Design Veriflcation of an actual SDS subsystem are used to illustrate the beneflts and limitations of the current implementation of the formal method. Finally, the paper discusses related work, draws conclusions regarding the efiectiveness of the method and examines how its limitations can be addressed by further theoretical and applied work.