Construction of CFC-Programs by LTL-Specification

Abstract

This article continues a cycle of papers, which describe an approach to construction and verification of discrete PLC-programs by an LTL-specification. The approach provides a possibility of PLC-program correctness analysis by the model checking method. For the specification of the program behaviour the linear-time temporal logic LTL is used. The correctness analysis of an LTL specification is performed automatically by the symbolic model checking tool Cadence SMV. It was previously shown how ST-, LD- and IL-programs are constructed by a correct (with verified program properties) LTL-specification. In this article, a technology of CFC-program construction by an LTL-specification is described. The language CFC (Continuous Function Chart) is a variation of FBD (Function Block Diagram). FBD is a graphical language for microcircuits. CFC provides a possibility of free allocation of program components and connections on a screen. The approach to construction of CFC-programs is shown by an example. PLC-program representation on CFC within the approach to programming by LTLspecification differs from other representations. It gives the visualization of a data flow from inputs to outputs. The influence and dependence among variables is explicitly shown during the program execution within one PLC working cycle. In fact, CFC-program is a scheme of PLC-program data flow.