This paper describes a formal safety analysis technique which is demonstrated by performing empirical formal safety analysis with the case study of beamline hutch door Interlock system that is developed by using PLC (Programmable Logic Controller) systems at the Pohang Accelerator Laboratory. In order to perform formal safety analysis, we have built the Z formal specifications representation from user requirement written in ambiguous natural language and target PLC ladder logic, respectively. We have also studied the effective method to express typical PLC timer component by using specific Z formal notation which is supported by temporal history. We present a formal proof technique specifying and verifying that the hazardous states are not introduced into ladder logic in the PLC-based safety critical system. And also, we have found that some errors or mismatches in user requirement and final implemented PLC ladder logic while analyzing the process of the consistency and completeness of Z translated formal specifications. In the case of relatively small systems like Beamline hutch door interlock system, a formal safety analysis including explicit proof is highly recommended so that the safety of PLC-based critical system may be enhanced and guaranteed. It also provides a helpful benefits enough to comprehend user requirement expressed by ambiguous natural language.
본 논문에서는 정형적 PLC 기반 안전필수계통인 포항방사광가속기 빔라인 허치문 연동계통에 대하여 정형적인 안전성 분석을 수행하였다. 정형적 안전성 분석을 수행하기 위해 애매모호한 자연언어로 표기된 사용자의 설계요구 사양과 PLC 래더 프로그램 각각으로부터 Z 정형 명세언어를 활용하여, 정형화 변형작업을 수행하였다. 또한 대표적인 PLC 타이머 소자에 대한 충실한 Z 표현을 위하여 시간적인 이력성분을 갖는 특정 Z 정형표기기법을 응용하였다. 본 연구의 결과로 PLC 기반 안전필수계통에 있어서 래더(Ladder) 프로그램내에 위험한 상황이 존재하지 않음을 수학적으로 입증하고 확인할 수 있는 정형적 증명기법을 제안할 수 있었다.
또한 양방향으로 변환된 Z 정형 명세언어상에서 일치성 및 완벽성을 확인하는 과정중, 사용자 요구명세 사양과 최종 설치된 PLC 래더 프로그램사이에서 상호 일치하지 않는 내용 및 일부 설계결함을 발견할 수 있었다.
본 연구를 통하여 빔라인 허치문 연동계통과 같이 비교적 작은 규모의 PLC 기반 안전필수계통에 대해서는 안전성을 향상시키고 보증하기 위한 방법으로 명확한 수학적 증명방법에 의한 정형적 안전성 분석이 필요한 것으로 제안할 수 있었으며, 동시에, 애매모호한 자연언어로 표현된 사용자 설계요구 사양에 대한 효과적인 이해가 정형화 분석 작업을 통해 이루어질 수 있음을 확인하였다.
