Application of Tabular Methods to the Specification and Verification of a Nuclear Reactor Shutdown System

by M. Lawford, P. Froebel and G. Moum

Abstract: This paper describes the use of tabular methods at Ontario Power Generation Inc.\ (OPGI) \footnote{Ontario Power Generation Inc.\ is the electricity generation company created from Ontario Hydro on April 1, 1999.} on the Darlington Nuclear Generating Station Shutdown System (SDS) Trip Computer Software Redesign Project. We first motivate the selection of tabular methods and provide an overview of the Systematic Design Verification (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 Verification of an actual SDS subsystem are used to illustrate the benefits and limitations of the current implementation of the formal method. Finally, the paper discusses related work, draws conclusions regarding the effectiveness of the method and examines how its limitations can be addressed by further theoretical and applied work.


Download

tables.ps (391k, postscript) OR tables.pdf (446k, PDF)


BibTeX Entry

@Unpublished{LawFroMou00,
  author =	 {M. Lawford and P. Froebel and G. Moum},
  title =	 {Application of Tabular Methods to the Specification
                  and Verification of a Nuclear Reactor Shutdown
                  System},
  journal =	 {Formal Methods in System Design},
  note =	 {Submitted to Formal Methods in System Design}
}


[ CAS | ML | Papers ]


Mark Lawford
Last modified: Tue Aug 21 11:54:19 EDT 2001