A Systematic Approach to Safety Verification of Function Block Diagrams
As a Programmable logic controller (PLC)is often used to implement safety-critical embedded software, rigorous safety demonstration of PLC code is indispensible. Function block diagram (FBD)is a standard application programming language for the PLC and currently being used in the development of a fully-digitalized reactor protection system (RPS), which is called IDiPS, under the Korea Nuclear Instrumentation & Control System (KNICS)project. Therefore, Safety verification issue of FBD programs is a pressing problem, and hence of great importance. In this paper, we propose two methods for safety verification of FBDs as an integrated manner: Formal verification method with model checking technique and Software safety analysis (SSA)method with software fault tree analysis (SFTA) technique. Firstly, we propose a formal verification method of FBD programs;FBD programs are defined formally in compliance with IEC 61131-3. and then the programs are automatically translated into Verilog model by the supporting tool, FBD2V, which is developed to support the FBD verification framework, and finally the model is verified using Cadence SMV, and counterexamples are displayed in the form of timing graph to enhance their readability. Secondly, we propose a SFTA technique on function block diagrams as a SSA method;we define fault tree templates for each FBD function block and propose a semi-automatic FTA process to do safety analysis of FBD programs efficiently and correctly. The proposed approach was applied to real FBD codes of KNICS RPS and it showed that it was applicable to real-world systems.
Function block diagram (FBD) Programmable logic controller (PLC) Formal Verification Model checking Software safety analysis (SSA) Software fault tree analysis (SFTA)
Koh Kwang Yong Seong Poong Hyun Jee Eun Kyoung Cha Sung Deok Park Gee Yong
Department of Nuclear & Quantum Engineering, Korea Advanced Institute of Science and Technology (KAI Division of Computer Science, EECS Department, KAIST, Daejeon 305-701, Korea I&C and Human Factors Center, Korea Atomic Energy Research Institute (KAERI), Daejeon, Korea
国际会议
ISSNP2008、CSEPC、ISOFIC2008(第二届21世纪和谐核电系统国际会议、第四届电厂控制中认知系统工程方法国际会议暨第三届未来核电厂仪表与控制国际会议)
哈尔滨
英文
553-561
2008-09-08（万方平台首次上网日期，不代表论文的发表时间）