О выразительности подхода к построению ПЛК-программ по LTL-спецификации


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

Полный текст:


Аннотация

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


Об авторах

Е. В. Кузьмин
Ярославский государственный университет им. П.Г. Демидова
Россия

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

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



Д. А. Рябухин
Ярославский государственный университет им. П.Г. Демидова
Россия

 аспирант

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



В. А. Соколов
Ярославский государственный университет им. П.Г. Демидова
Россия

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

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



Список литературы

1. Кузьмин Е.В., Рябухин Д.А., Соколов В.А., “Моделирование согласованного поведения ПЛК-датчиков”, Моделирование и анализ информационных систем, 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).]

2. Рябухин Д.А., Кузьмин Е.В., Соколов В.А., “Построение 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).]

3. Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация 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).]

4. Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация ПЛК-программ по 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).]

5. Кузьмин Е.В., Соколов В.А., “Моделирование, спецификация и построение программ логических контроллеров”, Моделирование и анализ информационных систем, 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).]

6. Минский М., Вычисления и автоматы, М.: Мир, 1971; [Minsky M., Computation: Finite and Infinite Machines, Prentice-Hall, Inc., 1967.]

7. Петров И.В., Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования, М.: СОЛОН-Пресс, 2004; [Petrov I.V., Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija, M.: SOLON-Press, 2004, (in Russian).]

8. Baier C., Katoen J.-P., Principles of Model Checking, The MIT Press, 2008.

9. Clark E. M., Grumberg O., Peled D. A., Model Checking, The MIT Press, 2001.

10. CoDeSys, Controller Development System, http://www.3s-software.com/.

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

12. Kuzmin E. V., Sokolov V. A., “Modeling, Specification and Construction of PLC-rograms”, Automatic Control and Computer Sciences, 48:7 (2014), 554–563.

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

14. Parr E. A., Programmable Controllers. An engineer’s guide, Newnes, 2003.

15. Schroeppel R., A Two Counter Machine Cannot Calculate 2N, Memo 257. Massachusetts Institute of Technology, Artificial Intelligence Laboratory, 1972.

16. SMV, The Cadence SMV Model Checker, http://www.kenmcmil.com/smv.html.


Дополнительные файлы

Для цитирования: Кузьмин Е.В., Рябухин Д.А., Соколов В.А. О выразительности подхода к построению ПЛК-программ по LTL-спецификации. Моделирование и анализ информационных систем. 2015;22(4):507-520. https://doi.org/10.18255/1818-1015-2015-4-507-520

For citation: Kuzmin E.V., Ryabukhin D.A., Sokolov V.A. On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification. Modeling and Analysis of Information Systems. 2015;22(4):507-520. (In Russ.) https://doi.org/10.18255/1818-1015-2015-4-507-520

Просмотров: 356

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)