maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2015-4-507-520mais-269Research ArticleОригинальные статьиArticlesО выразительности подхода к построению ПЛК-программ по LTL-спецификацииOn the Expressiveness of the Approach to Constructing PLC-programs by LTL-SpecificationКузьминЕ. В.KuzminE. V.

доктор физ.-мат. наук, доцент, профессор кафедры теоретической информатики

ул. Советская, 14, г. Ярославль, 150000 Россия

doctor of science, associate professor

Sovetskaya str., 14, Yaroslavl, 150000, Russia

kuzmin@uniyar.ac.ruРябухинД. А.RyabukhinD. A.

 аспирант

ул. Советская, 14, г. Ярославль, 150000 Россия

graduate student

Sovetskaya str., 14, Yaroslavl, 150000, Russia

dmitriy_ryabukhin@mail.ruСоколовВ. А.SokolovV. A.

доктор физ.-мат. наук, профессор, зав. кафедрой теоретической информатики

ул. Советская, 14, г. Ярославль, 150000 Россия,

doctor of science, professor

Sovetskaya str., 14, Yaroslavl, 150000, Russia

sokolov@uniyar.ac.ruЯрославский государственный университет им. П.Г. ДемидоваРоссияP.G. Demidov Yaroslavl State UniversityRussian Federation201520082015224507520Copyright © Кузьмин Е.В., Рябухин Д.А., Соколов В.А., 20152015Кузьмин Е.В., Рябухин Д.А., Соколов В.А.Kuzmin E.V., Ryabukhin D.A., Sokolov V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/269

Статья посвящена подходу к построению и верификации «дискретных» программ логических контроллеров (ПЛК) по LTL-спецификации. Этот подход обеспечивает возможность анализа корректности программ логических контроллеров с помощью метода проверки модели (Model Checking). В рамках подхода в качестве языка спецификации программного поведения используется язык темпоральной логики LTL. Анализ корректности LTL-спецификации относительно программных свойств производится автоматически с помощью программного средства символьной проверки модели Cadence SMV. В статье демонстрируется состоятельность подхода к построению и верификации ПЛК-программ по LTL-спецификации с точки зрения тьюринговой мощности. Доказывается, что в соответствии с этим подходом для произвольной счётчиковой машины Минского может быть построена LTL-спецификация, по которой осуществляется её программная реализация на любом из языков программирования ПЛК стандарта МЭК 61131-3. Поскольку счётчиковые машины Минского равномощны машинам Тьюринга, то и рассматриваемый подход к программированию ПЛК будет обладать тьюринговой мощностью. В доказательстве основное внимание уделяется заданию поведения счётчиковой машины в виде набора LTL-формул и сопоставлению этим формулам конструкций языков ST и SFC. SFC представляет интерес с точки зрения специфики графического языка, а язык ST рассматривается в качестве базового в том смысле, что реализация счётчиковой машины на языках IL, FBD/CFC и LD сводится к переписыванию на них конструкций ST-программы. Идея доказательства демонстрируется на примере трехсчетчиковой машины Минского, реализующей функцию возведения числа в квадрат.

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.

программируемые логические контроллеры (ПЛК)построение и верификация ПЛК-программLTL-спецификациясчётчиковые машины Минскогоprogrammable logic controllers (PLC)construction and verification of PLC-programsLTL-specificationMinsky counter machinesReferencesКузьмин Е.В., Рябухин Д.А., Соколов В.А., “Моделирование согласованного поведения ПЛК-датчиков”, Моделирование и анализ информационных систем, 21:4 (2014), 75–90; [Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “Modeling a Consistent Behavior of PLC-Sensors”, Modeling and Analysis of Information Systems, 21:4 (2014), 75–90, (in Russian).]Кузьмин Е.В., Рябухин Д.А., Соколов В.А., “Моделирование согласованного поведения ПЛК-датчиков”, Моделирование и анализ информационных систем, 21:4 (2014), 75–90; [Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “Modeling a Consistent Behavior of PLC-Sensors”, Modeling and Analysis of Information Systems, 21:4 (2014), 75–90, (in Russian).]Рябухин Д.А., Кузьмин Е.В., Соколов В.А., “Построение IL-программ ПЛК по LTL- спецификации”, Моделирование и анализ информационных систем, 21:2 (2014), 26– 38; [Ryabukhin D. A., Kuzmin E. V., Sokolov V. A., “Construction of PLC IL-programs by LTL-specification”, Modeling and Analysis of Information Systems, 21:2 (2014), 26–38, (in Russian).]Рябухин Д.А., Кузьмин Е.В., Соколов В.А., “Построение IL-программ ПЛК по LTL- спецификации”, Моделирование и анализ информационных систем, 21:2 (2014), 26– 38; [Ryabukhin D. A., Kuzmin E. V., Sokolov V. A., “Construction of PLC IL-programs by LTL-specification”, Modeling and Analysis of Information Systems, 21:2 (2014), 26–38, (in Russian).]Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация LD- программ ПЛК по LTL-спецификации”, Моделирование и анализ информационных систем, 20:6 (2013), 78–94; [Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC LD-programs by LTL-specification”, Modeling and Analysis of Information Systems, 20:6 (2013), 78–94, (in Russian).]Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация LD- программ ПЛК по LTL-спецификации”, Моделирование и анализ информационных систем, 20:6 (2013), 78–94; [Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC LD-programs by LTL-specification”, Modeling and Analysis of Information Systems, 20:6 (2013), 78–94, (in Russian).]Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация ПЛК-программ по LTL-спецификации”, Моделирование и анализ информационных систем, 20:4 (2013), 5–22; [Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC-programs by LTL-specification”, Modeling and Analysis of Information Systems, 20:4 (2013), 5–22, (in Russian).]Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация ПЛК-программ по LTL-спецификации”, Моделирование и анализ информационных систем, 20:4 (2013), 5–22; [Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC-programs by LTL-specification”, Modeling and Analysis of Information Systems, 20:4 (2013), 5–22, (in Russian).]Кузьмин Е.В., Соколов В.А., “Моделирование, спецификация и построение программ логических контроллеров”, Моделирование и анализ информационных систем, 20:2 (2013), 104–120; [Kuzmin E. V., Sokolov V. A., “Modeling, Specification and Construction of PLC-programs”, Modeling and Analysis of Information Systems, 20:2 (2013), 104–120, (in Russian).]Кузьмин Е.В., Соколов В.А., “Моделирование, спецификация и построение программ логических контроллеров”, Моделирование и анализ информационных систем, 20:2 (2013), 104–120; [Kuzmin E. V., Sokolov V. A., “Modeling, Specification and Construction of PLC-programs”, Modeling and Analysis of Information Systems, 20:2 (2013), 104–120, (in Russian).]Минский М., Вычисления и автоматы, М.: Мир, 1971; [Minsky M., Computation: Finite and Infinite Machines, Prentice-Hall, Inc., 1967.]Минский М., Вычисления и автоматы, М.: Мир, 1971; [Minsky M., Computation: Finite and Infinite Machines, Prentice-Hall, Inc., 1967.]Петров И.В., Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования, М.: СОЛОН-Пресс, 2004; [Petrov I.V., Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija, M.: SOLON-Press, 2004, (in Russian).]Петров И.В., Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования, М.: СОЛОН-Пресс, 2004; [Petrov I.V., Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija, M.: SOLON-Press, 2004, (in Russian).]Baier C., Katoen J.-P., Principles of Model Checking, The MIT Press, 2008.Baier C., Katoen J.-P., Principles of Model Checking, The MIT Press, 2008.Clark E. M., Grumberg O., Peled D. A., Model Checking, The MIT Press, 2001.Clark E. M., Grumberg O., Peled D. A., Model Checking, The MIT Press, 2001.CoDeSys, Controller Development System, http://www.3s-software.com/.CoDeSys, Controller Development System, http://www.3s-software.com/.Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC LD Programs by the LTL Specification”, Automatic Control and Computer Sciences, 48:7 (2014), 424–436.Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC LD Programs by the LTL Specification”, Automatic Control and Computer Sciences, 48:7 (2014), 424–436.Kuzmin E. V., Sokolov V. A., “Modeling, Specification and Construction of PLC-rograms”, Automatic Control and Computer Sciences, 48:7 (2014), 554–563.Kuzmin E. V., Sokolov V. A., “Modeling, Specification and Construction of PLC-rograms”, Automatic Control and Computer Sciences, 48:7 (2014), 554–563.Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “Modeling a Consistent Behavior of PLC-Sensors”, Automatic Control and Computer Sciences, 48:7 (2014), 602–614.Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “Modeling a Consistent Behavior of PLC-Sensors”, Automatic Control and Computer Sciences, 48:7 (2014), 602–614.Parr E. A., Programmable Controllers. An engineer’s guide, Newnes, 2003.Parr E. A., Programmable Controllers. An engineer’s guide, Newnes, 2003.Schroeppel R., A Two Counter Machine Cannot Calculate 2N, Memo 257. Massachusetts Institute of Technology, Artificial Intelligence Laboratory, 1972.Schroeppel R., A Two Counter Machine Cannot Calculate 2N, Memo 257. Massachusetts Institute of Technology, Artificial Intelligence Laboratory, 1972.SMV, The Cadence SMV Model Checker, http://www.kenmcmil.com/smv.html.SMV, The Cadence SMV Model Checker, http://www.kenmcmil.com/smv.html.

The authors declare that there are no conflicts of interest present.