Model-to-Model Transformation Of Nuclear Industry I&C Logic To Assist Model Checking

Abstract

The demand for electricity has increased proportionately with massive urbanisation and in-dustrialisation. Nuclear energy is a strong candidate which can be one of the solutions to ca-ter to this massive demand for energy. Nuclear resources have the benefit of enormous ener-gy density, low carbon footprint, cheap operating cost and production reliability. Even though it is deemed as a dependable and economically viable option, it is limited by safety concerns, unfortunate accidents can cause monumental and long-lasting consequences. On the other hand, if critically examined, thoroughly tested and flawlessly implemented, the decision-makers can opt for nuclear source. Thus utilising nuclear resources will call for an error-proof instrumentation and control system to observe and ensure safe operation. Model verification plays a vital role in critical analysis of I & C system, it checks all the possibilities the system may reach, and thus provide a model to develop an I&C safety system.

An industrial operation may suffer from unknown component failure and design error, but its safety-critical system must be able to strictly prohibit these undesired events in the system before causing any major accident. “Model Checking” is a mathematical deterministic tool for logic design verification, which has been proven to be effective for detecting design errors in the system. Granted that, Instrumentation and control system starts with logic design at the preliminary phase, a model checking tool can efficiently identify design faults by exhaustive analysis. NuSMV is such a tool, which provides simpler syntax, that can represent the system as logical states with simple data structures. Analysts write SMV files to represent the system available as proprietary non-standard machine-readable diagrams. This thesis proposes an automation step towards diagram import in a verification tool and implements an intermediate data representation.

This thesis provides a perception of various technologies relevant to broader authentication process of a safety system covering from design to verification tools. The state-of-the-art model-checking practice is discussed briefly. Subsequently, a number of logical instrumenta-tion and control diagrams, drawn in Microsoft VISIO tool, are analysed and processed to au-tomatically create an intermediate component network consisting of Function Block elements. A significant effort is spent to partially generate NuSMV code from the retrieved component data to assist the model checking of the system. Finally, the thesis is concluded with a synop-sis of the work done and future development scope.