Software quality assurance is important for the development and approval of an safety-critical system. Formal methods supports specifying the requirements unambiguously and proving the properties of it for quality assurance. While formal methods claims to be an promising technique, there have been few examples of successful applications of it in practice.
We specify the requirements of Wolsung NPP shutdown system number 2(SDS 2) and verify it using PVS which is a tool for formal methods. SDS 2 is a safety-critical system which prevents the atomic furnace from being in the abnormal conditions. We prove the correctness of this system using PVS so that we can guarantee the quality of it. We also show the usability of formal methods by comparing with fagan inspection.
