RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Model. Anal. Inform. Sist.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Model. Anal. Inform. Sist., 2016, Volume 23, Number 2, Pages 173–184 (Mi mais489)  

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

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 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.

Keywords: programmable logic controllers (PLC), construction and verification of PLC-programs, LTL-specification, CFC-diagrams.

Funding Agency Grant Number
Russian Foundation for Basic Research 12-01-00281_a
This work was supported by the Russian Foundation for Basic Research (RFBR), №12-01-00281-a.


DOI: https://doi.org/10.18255/1818-1015-2016-2-173-184

Full text: PDF file (309 kB)
References: PDF file   HTML file

Bibliographic databases:

UDC: 517.9
Received: 01.03.2016

Citation: 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
\Bibitem{RyaKuzSok16}
\by D.~A.~Ryabukhin, E.~V.~Kuzmin, V.~A.~Sokolov
\paper Construction of CFC-programs by LTL-specification
\jour Model. Anal. Inform. Sist.
\yr 2016
\vol 23
\issue 2
\pages 173--184
\mathnet{http://mi.mathnet.ru/mais489}
\crossref{https://doi.org/10.18255/1818-1015-2016-2-173-184}
\mathscinet{http://www.ams.org/mathscinet-getitem?mr=3504587}
\elib{http://elibrary.ru/item.asp?id=25810350}


Linking options:
  • http://mi.mathnet.ru/eng/mais489
  • http://mi.mathnet.ru/eng/mais/v23/i2/p173

    SHARE: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Моделирование и анализ информационных систем
    Number of views:
    This page:228
    Full text:87
    References:30

     
    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2020