The Computerized Procedure System (CPS) is one of the primary operating support systems in the digital Main Control Room. CPS displays procedure on the computer screen in the form of a flow chart and displays plant operating information along with procedure in-structions. It also supports operator decision making by providing a system decision. A pro-cedure flow should be correct and reliable, as an error would lead to operator misjudgment and inadequate control. In this paper we present a modeling for CPS that enables formal veri-fication based on Petri nets. The proposed State Token Petri Net(STPN) also support model-ing of a procedure flow that has various interruptions by the operator according to the plant condition. STPN modeling is compared with Coloured Petri net when they are applied to Emergency Operating Computerized Procedure. A converting program for Computerized Procedure (CP) to STPN has been also developed. The formal verification and validation method of CP with STPN increase the safety of nuclear power plant and provide digital quali-ty assurance means that is needed when the role and function of CPS is increasing.
디지털 주 제어실에는 여러 가지 운전지원시스템의 일환으로 전산화절차서가 적용되어 있다. 전산화절차서는 운전절차서를 흐름도와 유사한 형태로 제공하고 절차수행 시 필요한 운전정보와 운전수단을 절차서와 함께 제공한다. 또한 운전에 필요한 판단을 지원하여 운전원이 절차서의 흐름에 따라 절차서를 수행할 수 있도록 지원한다. 전산화절차서는 흐름을 내포하고 있기 때문에, 만약 흐름에 오류가 있을 경우 운전원을 잘못된 운전 흐름으로 유도할 수 있다. 따라서 본 연구에서는 절차서의 흐름이 건전함을 확인할 수 있는 확인 방법을 제시하였다. 기존에 소프트웨어의 확인 검증에 사용되는 정형검증기법 중 하나인 페트리넷을 전산화절차서 확인에 사용할 수 있도록, 전산화절차서를 색갈 페트리넷으로 변환하는 법칙과 변환하는 프로그램을 제시하였다. 제시된 방법에 따라 신고리3&4 비상운전절차서를 대상으로 변환 및 확인을 수행하였다. 제시된 방법은 절차서의 흐름 구조가 건전한지 확인할 수 있는 방법을 제시하였다. 또한 전산화절차서는 운전원이 발전소의 상태에 따라 흐름을 변경하여 수행 할 수 있다. 이에 대한 모델링은 기존의 색깔 페트리넷을 적용하는 데에 모델이 너무 복잡해 지는 한계가 있다. 따라서 본 연구에서는 상태 토큰 페트리넷 모델링 방법을 제시하였으며 이를 통하여 운전원이 흐름을 변경하는 경우에도 전산화절차서의 흐름에 포함되는 오류를 찾아낼 수 있다. 제안된 상태토큰페트리넷은 전산화절차서의 확인뿐만 아니라, 복잡한 흐름을 갖는 경우에 적용될 수 있을 것이다.
