(A) formal safety analysis for PLC software-based safety critical system using Z = Z언어를 이용한 PLC기반 안전필수 계통에 대한 정형적 안전성분석

Cited 0 time in webofscience Cited 0 time in scopus
  • Hit : 342
  • Download : 0
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.
Advisors
Seong, Poong-Hyunresearcher성풍현researcher
Description
한국과학기술원 : 원자력공학과,
Publisher
한국과학기술원
Issue Date
1997
Identifier
114534/325007 / 000933014
Language
eng
Description

학위논문(석사) - 한국과학기술원 : 원자력공학과, 1997.2, [ iv, 57 p. ]

Keywords

Safety analysis; Formal; Safety critical; PLC; 안전성분석; 정형적; 안전필수; Z

URI
http://hdl.handle.net/10203/49362
Link
http://library.kaist.ac.kr/search/detail/view.do?bibCtrlNo=114534&flag=dissertation
Appears in Collection
NE-Theses_Master(석사논문)
Files in This Item
There are no files associated with this item.

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0