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


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
Issue number3
Publication statusPublished - 1998 Dec 1
Externally publishedYes



  • 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