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

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

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.