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

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