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., 2015, Volume 22, Number 4, Pages 507–520 (Mi mais456)  

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

On the expressiveness of the approach to constructing PLC-programs by LTL-specification

E. V. Kuzmin, D. A. Ryabukhin, V. A. Sokolov

P.G. Demidov Yaroslavl State University, Sovetskaya str., 14, Yaroslavl, 150000, Russia

Abstract: The article is devoted to the approach to constructing and verification of discrete PLC-programs by LTL-specification. This approach provides an ability of correctness analysis of PLC-programs by the model checking method. The linear temporal logic LTL is used as a language of specification of the program behavior. The correctness analysis of LTL-specification is automatically performed by the symbolic model checking tool Cadence SMV.
The article demonstrates the consistency of the approach to constructing and verification of PLC programs by LTL-specification from the point of view of Turing power. It is proved, that in accordance with this approach for any Minsky counter machine can be built an LTL-specification, which is used for machine implementation in any PLC programming language of standard IEC 61131-3. Minsky machines equipollent Turing machines, and the considered approach also has Turing power.
The proof focuses on representation of a counter machine behavior in the form of a set of LTL-formulas and matching these formulas to constructions of ST and SFC languages. SFC is interesting as a specific graphical language. ST is considered as a basic language because an implementation of a counter machine in IL, FBD/CFC and LD languages is reduced to rewriting blocks of ST-program.
The idea of the proof is demonstrated by an example of a Minsky 3-counter machine, which implements a function of squaring.

Keywords: programmable logic controllers (PLC), construction and verification of PLC-programs, LTL-specification, Minsky counter machines.

Funding Agency Grant Number
Russian Foundation for Basic Research 12-01-00281-a


DOI: https://doi.org/10.18255/1818-1015-2015-4-507-520

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

Bibliographic databases:

UDC: 517.9
Received: 03.08.2015

Citation: E. V. Kuzmin, D. A. Ryabukhin, V. A. Sokolov, “On the expressiveness of the approach to constructing PLC-programs by LTL-specification”, Model. Anal. Inform. Sist., 22:4 (2015), 507–520

Citation in format AMSBIB
\Bibitem{KuzRyaSok15}
\by E.~V.~Kuzmin, D.~A.~Ryabukhin, V.~A.~Sokolov
\paper On the expressiveness of the approach to constructing PLC-programs by LTL-specification
\jour Model. Anal. Inform. Sist.
\yr 2015
\vol 22
\issue 4
\pages 507--520
\mathnet{http://mi.mathnet.ru/mais456}
\crossref{https://doi.org/10.18255/1818-1015-2015-4-507-520}
\mathscinet{http://www.ams.org/mathscinet-getitem?mr=3418470}
\elib{http://elibrary.ru/item.asp?id=24273051}


Linking options:
  • http://mi.mathnet.ru/eng/mais456
  • http://mi.mathnet.ru/eng/mais/v22/i4/p507

    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

    This publication is cited in the following articles:
    1. D. A. Ryabukhin, E. V. Kuzmin, V. A. Sokolov, “Postroenie CFC-programm PLK po LTL-spetsifikatsii”, Model. i analiz inform. sistem, 23:2 (2016), 173–184  mathnet  crossref  mathscinet  elib
  • Моделирование и анализ информационных систем
    Number of views:
    This page:161
    Full text:46
    References:23

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