An algebraic approach for PLC programs verification

This article presents a verification based on a specific Boolean algebra, called II, and symbolic reasoning on equations defined in this algebra. The formal definition of this algebra enables to model binary signals that include variables states, events, as well as physical delays between events. The behavior of the generic function blocks of the IEC 61131 standard as well as of PLC programs using these function blocks can be described in this algebra. Properties proof on PLC programs is performed by demonstrating, from the program, the formulas that express in the II algebra the properties to be proved.