METHOD OF AUTHETICATING INTERLOCK FUNCTION OF PLC CONTROL PROGRAM USING SMV

摘要

Provided is a method of verifying an interlock function of a PLC control program which includes transforming the PLC control program into a control intermediate model, simplifying the control intermediate model using information on an output signal list of output signals among a plurality of output signals outputted from the PLC driving system as the PLC control program is driven, transforming the PLC driving system and the simplified control intermediate model into a finite state machine (FSM) form, and verifying in relays of checking whether a situation in which the output signals of the output signal list causing the erroneous situation are turned on (ON) at the same time occurs in the control intermediate model simplified to the FSM form using a symbolic model verifier (SMV) and modifying the PLC control program.

主权项

1. A method of verifying an interlock function of a PLC control program driven in a PLC driving system controlling an automated production system, the method comprising:
transforming the PLC control program into a control intermediate model in which an output signal is expressed as a parent node and state transformation logics having an effect on state transformation of the output signal are expressed as child nodes; simplifying the control intermediate model using information on an output signal list of output signals among a plurality of output signals outputted from the PLC driving system as the PLC control program is driven, which are turned on (ON) at the same time and cause an erroneous situation in operations of the automated production system; transforming the PLC driving system and the simplified control intermediate model into a finite state machine (FSM) form; and verifying in relays of checking whether a situation in which the output signals of the output signal list causing the erroneous situation are turned on (ON) at the same time occurs in the control intermediate model simplified to the FSM form using a symbolic model verifier (SMV) and modifying the PLC control program to provide the interlock function to prevent the occurrence of the erroneous situation.