A formal method framework for automated verification of a deaerator system

Nur Amirah , Othman (2014) A formal method framework for automated verification of a deaerator system. Project Report. UTeM. (Submitted)

Text A FORMAL METHOD FRAMEWORK FOR AUTOMATED VERIFICATION OF A DEAERATOR SYSTEM 24pages.pdf Download (859kB)

Abstract

Deaerator is important equipment in feed water system of a power plant. The role of deaerator system is to remove dissolved gases which are oxygen and carbon dioxide that comes from the water leaving of condenser and to give the adequate level of water to the deaerator storage tank. In deaerator system, the flow of steam and water has their own principles which are the flow of steam before supply to the deaerator storage tank and the flow of water from condenser flow before supply to the boiler. The principle of deaerator system must in the correct order to make sure it is in the safe condition to the plant system. Thus, formal verification of correctness of a property is used as an approach to ensure all the specification created meets the actual behavior for the system. All the specifications must always hold during the verification process to ensure that the model designed will not violate. The verification procedure is also need to eliminate the errors that decrease the safety of the automation system. Hence, in this project, it will show on how the computational method such as temporal logic model checking can be used to verify the correctness of the design of an automation system. The project involves the deaerator model and the design of the ladder diagram (LD) using Programmable Logic Controller (PLC). The project used Computational Tree Logic (CTL) as the temporal logic to determine the specification. By using several logical specifications to the deaerator system, the designed model of deaerator model and control logic should verify so that it will not violate the required specification. If none of the behaviors of the system violates the given specification, the model of the system will correct. Otherwise, the model checker will automatically execute the counterexample of the model system to show why the specification is false. The verification of the system will be performed by using Symbolic Model Verify (SMV) model checker software.

Actions (login required)

View Item