Modelirovanie i Analiz Informatsionnykh Sistem
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


Modelirovanie i Analiz Informatsionnykh Sistem, 2016, Volume 23, Number 2, Pages 173–184
DOI: https://doi.org/10.18255/1818-1015-2016-2-173-184
(Mi mais489)
 

This article is cited in 1 scientific paper (total in 1 paper)

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
Full-text PDF (309 kB) Citations (1)
References:
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.
Received: 01.03.2016
Bibliographic databases:
Document Type: Article
UDC: 517.9
Language: Russian
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://mathscinet.ams.org/mathscinet-getitem?mr=3504587}
\elib{https://elibrary.ru/item.asp?id=25810350}
Linking options:
  • https://www.mathnet.ru/eng/mais489
  • https://www.mathnet.ru/eng/mais/v23/i2/p173
  • This publication is cited in the following 1 articles:
    Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Моделирование и анализ информационных систем
    Statistics & downloads:
    Abstract page:535
    Full-text PDF :717
    References:67
     
      Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024