Formal Verification of Logic Control Systems with Nondeterministic Behaviors

This paper describes a formal modeling and verification of an arm pick-and-place system, in which nondeterministic behaviors of the arm state condition and timer function blocks are applied. We design an appropriate PLC program using a ladder diagram (LD) for the arm pick-and-place operation and apply in it a situation where the arm may drop the product or material being gripped because of an external force. In addition, the timer function blocks are used with formalization of their finite-state logical properties. We use an actual model of the arm to verify that safe operations are established for normal product pick-and-place, as well as when the product has fallen. In addition, we perform arm model verifications for five important temporal properties using the NuSMV model checker. We present two types of experiments to validate the safety of the designed LD program. We also verify that the nondeterminism that appears as a result of the system behaviors can be formalized and used to represent logical assumptions for the properties that need to be verified