Construction of CFC-programs by LTL-specification
D. A. Ryabukhin, E. V. Kuzmin, V. A. Sokolov
P.G. Demidov Yaroslavl State University, Sovetskaya str., 14, Yaroslavl, 150000, Russia
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 behavior 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.
Previously it was 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 LTL-specification differs from other representations. It gives the visualisation of a data flow from inputs to outputs. Influence and dependence between variables is explicitly shown during program execution within one PLC working cycle. In fact, CFC-program is a scheme of PLC-program data flow.
programmable logic controllers (PLC), construction and verification of PLC-programs, LTL-specification, CFC-diagrams.
PDF file (309 kB)
D. A. Ryabukhin, E. V. Kuzmin, V. A. Sokolov, “Construction of CFC-programs by LTL-specification”, Model. Anal. Inform. Sist., 23:2 (2016), 173–184
Citation in format AMSBIB
\by D.~A.~Ryabukhin, E.~V.~Kuzmin, V.~A.~Sokolov
\paper Construction of CFC-programs by LTL-specification
\jour Model. Anal. Inform. Sist.
Citing articles on Google Scholar:
Related articles on Google Scholar:
|Number of views:|