Combining Software Methods for Effective Deployment of Programmable Logic Controllers (PLCs)

Summary This paper presents a preliminary study of an approach that models programmable logic controllers (PLCs) for their effective deployment in industrial control processes. A working model is developed for automatic allocation of PLCs and also a formal verification of Ladder Diagram representations of control processes using the Symbolic Model Verifier (SMV) tool. Automatic resource allocation is achieved through the proposition of a digraph model for any Ladder Diagram representation of a control process, which is then translated to an XML (Extensible Mark Up Language) model. The required PLC resources needed to implement a control process are extracted from the XML model. These resources are then used by a selection engine to determine, from a PLC database, the most appropriate PLCs or Embedded Controllers (EBCs) that can satisfy the resource requirements. Additionally, information extracted from the XML model is used to generate a formally verifiable SMV code of the system. This paper focuses on the practical implementation, testing, and verification of three conceptual modules applied to a control process. These are, the XML model of the control process, the PLC Database Automatic Resource Allocation, and the XML-to-SMV translator. This work was significantly motivated by the ever increasing number of industries who seek to increase their productivity by automating their processes.