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.

In an automated industry PLC plays a central role to control the manufacturing system. Therefore, fault free operation of PLC controlled manufacturing system is essential in order to maximize a firm's productivity. On the contrary, distributed nature of manufacturing system and growing complexity of the PLC programs presented a challenging task of designing a rapid fault finding system for an uninterrupted process operation. Hence, designing an intelligent monitoring, and diagnosis system is needed for smooth functioning of the operation process. In this paper, we propose a method to continuously acquire a stream of PLC signal data from the normal operational PLC-based manufacturing system and to generate diagnosis model from the observed PLC signal data. Consequently, the generated diagnosis model is used for distinguish the possible abnormalities of manufacturing system. To verify the proposed method, we provided a suitable case study of an assembly line.

가변단면 압출기술은 사용하는 금형의 조합에 의해 다양한 가공이 가능한 성형공법으로, 압출시에 금형의 움직임에 의하여 제품의 단면형상을 변화시키거나, 치수와 두께를 동시에 변화시킬 수 있다. 압출공정에서 압출속도, 압출압력, 압출온도는 압출품의 표면결함이나 내부품질에 있어 중요한 영향인자이다. 그중 일정한 압출속도는 균일한 메탈 플로를 형성하여 성형품질에 있어서 고른 상태를 유지하게 만드는 요소이다. 기존의 압출 성형에서 펌프토출양의 변화에 의한 추출속도변동 문제는 램 속도의 변화를 계측하고 토출 양을 조정함으로써 압출속도를 제어하는 방법으로 해결한다. 그러나 가변단면 압출공정에서는 제품의 단면형상의 변화에 따라 압출비가 변하므로 이에 따른 램 속도 제어가 있어야만 한다. 본 연구에서는 가변단면 압출공정에서 가공형상에 따른 제어 알고리즘을 제시하여 가변 형상에 따른 램의 이동 속도 및 위치를 제공하려 한다.