Earticle

초록

영어

In an automated industry PLC plays a central role to control the automation system. Therefore, fault free operation of PLC controlled automation system is essential in order to maximize a firm’s productivity. A prior test of control system is a practical way to check fault operations, but it is a time consuming job and can not check all possible fault operation. A formal verification of PLC program could be a best way to check all possible fault situation. Tracing the history of the study on formal verification, we found three problems, the first is that a formal representation of PLC control system is incomplete, the second is a state explosion problem and the third is that the verification result is difficult to use for the correction of control program. In this paper, we propose a transformation method to reproduce the control system correctly in formal model and efficient procedure to verify and correct the control program using verification result. To demonstrate the proposed method, we provided a suitable case study of an automation system.

목차

Abstract
 1. 서론
 2. SMV를 이용한 정형검증
 3. PLC 구동환경을 고려한 SMV 변환
 5. 타이머 시스템의 SMV 변환
 6. 인터록 검증
 7. 릴레이 검증 및 수정 기법
 8. 결론
 9. References

키워드

저자

• 박창목 [ Chang Mok Park | 인덕대학교 테크노경영과 ] Corresponding Author

참고문헌

발행기관

간행물

표지보기 관심저널 등록

• 간행물명

  대한안전경영과학회지 [Journal of Korea Safety Management & Science]

• 간기

  계간

• pISSN

  1229-6783

• eISSN

  2288-1484

• 수록기간

  1999~2025

• 십진분류

  KDC 530 DDC 620