Application of algebraic specification to verify the design of safety logic in nuclear power plants

Akira Fukumoto, Toshifumi Hayashi, Akihiko Ohsuga, Shinichi Honiden, Nobuyuki Mori

Research output: Contribution to journalArticle

Abstract

A formal verification method using an algebraic specification technique is proposed, and its effectiveness is studied. A computerized automatic verification system, which utilizes an algebraic specification to describe system requirements and to prove an inductive theorem based on a term-rewriting technique for verification, is built and evaluated through experimentally verifying the logic design of a digital reactor protection system in boiling water reactors. The results show that the proposed method can mathematically correctly verify the logic design in a limited time, thereby improving accuracy and reducing person-hours for the verification.

Original languageEnglish
Pages (from-to)255-263
Number of pages9
JournalNuclear Technology
Volume124
Issue number3
Publication statusPublished - 1998 Dec 1
Externally publishedYes

Fingerprint

nuclear power plants
Nuclear power plants
logic
specifications
Logic design
safety
logic design
Specifications
Boiling water reactors
boiling water reactors
theorems
reactors
requirements

Keywords

  • Algebraic specification
  • Digital safety systems
  • Verification and validation

ASJC Scopus subject areas

  • Nuclear and High Energy Physics
  • Nuclear Energy and Engineering
  • Condensed Matter Physics

Cite this

Application of algebraic specification to verify the design of safety logic in nuclear power plants. / Fukumoto, Akira; Hayashi, Toshifumi; Ohsuga, Akihiko; Honiden, Shinichi; Mori, Nobuyuki.

In: Nuclear Technology, Vol. 124, No. 3, 01.12.1998, p. 255-263.

Research output: Contribution to journalArticle

Fukumoto, A, Hayashi, T, Ohsuga, A, Honiden, S & Mori, N 1998, 'Application of algebraic specification to verify the design of safety logic in nuclear power plants', Nuclear Technology, vol. 124, no. 3, pp. 255-263.
Fukumoto, Akira ; Hayashi, Toshifumi ; Ohsuga, Akihiko ; Honiden, Shinichi ; Mori, Nobuyuki. / Application of algebraic specification to verify the design of safety logic in nuclear power plants. In: Nuclear Technology. 1998 ; Vol. 124, No. 3. pp. 255-263.
@article{4a029ac8614b4f0b80444e44e2a466fb,
title = "Application of algebraic specification to verify the design of safety logic in nuclear power plants",
abstract = "A formal verification method using an algebraic specification technique is proposed, and its effectiveness is studied. A computerized automatic verification system, which utilizes an algebraic specification to describe system requirements and to prove an inductive theorem based on a term-rewriting technique for verification, is built and evaluated through experimentally verifying the logic design of a digital reactor protection system in boiling water reactors. The results show that the proposed method can mathematically correctly verify the logic design in a limited time, thereby improving accuracy and reducing person-hours for the verification.",
keywords = "Algebraic specification, Digital safety systems, Verification and validation",
author = "Akira Fukumoto and Toshifumi Hayashi and Akihiko Ohsuga and Shinichi Honiden and Nobuyuki Mori",
year = "1998",
month = "12",
day = "1",
language = "English",
volume = "124",
pages = "255--263",
journal = "Nuclear Technology",
issn = "0029-5450",
publisher = "American Nuclear Society",
number = "3",

}

TY - JOUR

T1 - Application of algebraic specification to verify the design of safety logic in nuclear power plants

AU - Fukumoto, Akira

AU - Hayashi, Toshifumi

AU - Ohsuga, Akihiko

AU - Honiden, Shinichi

AU - Mori, Nobuyuki

PY - 1998/12/1

Y1 - 1998/12/1

N2 - A formal verification method using an algebraic specification technique is proposed, and its effectiveness is studied. A computerized automatic verification system, which utilizes an algebraic specification to describe system requirements and to prove an inductive theorem based on a term-rewriting technique for verification, is built and evaluated through experimentally verifying the logic design of a digital reactor protection system in boiling water reactors. The results show that the proposed method can mathematically correctly verify the logic design in a limited time, thereby improving accuracy and reducing person-hours for the verification.

AB - A formal verification method using an algebraic specification technique is proposed, and its effectiveness is studied. A computerized automatic verification system, which utilizes an algebraic specification to describe system requirements and to prove an inductive theorem based on a term-rewriting technique for verification, is built and evaluated through experimentally verifying the logic design of a digital reactor protection system in boiling water reactors. The results show that the proposed method can mathematically correctly verify the logic design in a limited time, thereby improving accuracy and reducing person-hours for the verification.

KW - Algebraic specification

KW - Digital safety systems

KW - Verification and validation

UR - http://www.scopus.com/inward/record.url?scp=0032298295&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0032298295&partnerID=8YFLogxK

M3 - Article

AN - SCOPUS:0032298295

VL - 124

SP - 255

EP - 263

JO - Nuclear Technology

JF - Nuclear Technology

SN - 0029-5450

IS - 3

ER -