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., 2013, Volume 20, Number 2, Pages 104–120 (Mi mais301)  

This article is cited in 6 scientific papers (total in 6 papers)

Modeling, Specification and Construction of PLC-programs

E. V. Kuzmin, V. A. Sokolov

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

Abstract: A new approach to construction of reliable discrete PLC-programs with timers — programming based on specification and verification — is proposed. Timers are modelled in a discrete way. For the specification of a program behavior we use the linear-time temporal logic LTL. Programming is carried out in the ST-language according to a LTL-specification. A new approach to programming of PLC is shown by an example.
The proposed programming approach provides an ability of a correctness analysis of PLC-programs using the model checking method. The programming requires fulfillment of the following two conditions: 1) a value of each variable should be changed not more than once per one full PLC-program implementation (per one full working cycle of PLC); 2) a value of each variable should only be changed in one place of a PLC-program.
Under the proposed approach the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations that increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value. The LTL-formulas (used for specification of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program, which satisfies temporal properties expressed by these formulas. Thus, the programming of PLC is reduced to the construction of LTL-specification of the behavior of each program variable.

Keywords: programmable pogic controllers, software engineering, modeling and specification of PLC-programs.

Full text: PDF file (200 kB)
References: PDF file   HTML file
UDC: 519.7
Received: 10.01.2013

Citation: E. V. Kuzmin, V. A. Sokolov, “Modeling, Specification and Construction of PLC-programs”, Model. Anal. Inform. Sist., 20:2 (2013), 104–120

Citation in format AMSBIB
\Bibitem{KuzSok13}
\by E.~V.~Kuzmin, V.~A.~Sokolov
\paper Modeling, Specification and Construction of PLC-programs
\jour Model. Anal. Inform. Sist.
\yr 2013
\vol 20
\issue 2
\pages 104--120
\mathnet{http://mi.mathnet.ru/mais301}


Linking options:
  • http://mi.mathnet.ru/eng/mais301
  • http://mi.mathnet.ru/eng/mais/v20/i2/p104

    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. E. V. Kuzmin, V. A. Sokolov, D. A. Ryabukhin, “Postroenie i verifikatsiya PLK-programm po LTL-spetsifikatsii”, Model. i analiz inform. sistem, 20:4 (2013), 5–22  mathnet
    2. E. V. Kuzmin, V. A. Sokolov, D. A. Ryabukhin, “Postroenie i verifikatsiya LD-programm PLK po LTL-spetsifikatsii”, Model. i analiz inform. sistem, 20:6 (2013), 78–94  mathnet
    3. D. A. Ryabukhin, E. V. Kuzmin, V. A. Sokolov, “Postroenie IL-programm PLK po LTL-spetsifikatsii”, Model. i analiz inform. sistem, 21:2 (2014), 26–38  mathnet
    4. E. V. Kuzmin, D. A. Ryabukhin, V. A. Sokolov, “Modelirovanie soglasovannogo povedeniya PLK-datchikov”, Model. i analiz inform. sistem, 21:4 (2014), 75–90  mathnet
    5. E. V. Kuzmin, D. A. Ryabukhin, V. A. Sokolov, “O vyrazitelnosti podkhoda k postroeniyu PLK-programm po LTL-spetsifikatsii”, Model. i analiz inform. sistem, 22:4 (2015), 507–520  mathnet  crossref  mathscinet  elib
    6. 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:367
    Full text:95
    References:45

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