Аннотация:
Статья посвящена подходу к построению и верификации «дискретных» программ логических контроллеров (ПЛК) по LTL-спецификации.
Этот подход обеспечивает возможность анализа корректности программ логических контроллеров с помощью метода проверки модели (Model Checking).
В рамках подхода в качестве языка спецификации программного поведения используется язык темпоральной логики LTL.
Анализ корректности LTL-спецификации относительно программных свойств производится автоматически с помощью программного средства символьной проверки модели Cadence SMV.
В статье демонстрируется состоятельность подхода к построению и верификации ПЛК-программ по LTL-спецификации с точки зрения тьюринговой мощности.
Доказывается, что в соответствии с этим подходом для произвольной счётчиковой машины Минского может быть построена LTL-спецификация, по которой осуществляется её программная реализация на любом из языков программирования ПЛК стандарта МЭК 61131-3. Поскольку счётчиковые машины Минского равномощны машинам Тьюринга, то и рассматриваемый подход к программированию ПЛК будет обладать тьюринговой мощностью.
В доказательстве основное внимание уделяется заданию поведения счётчиковой машины в виде набора LTL-формул и сопоставлению этим формулам конструкций языков ST и SFC.
SFC представляет интерес с точки зрения специфики графического языка, а язык ST рассматривается в качестве базового в том смысле, что реализация счётчиковой машины на языках IL, FBD/CFC и LD
сводится к переписыванию на них конструкций ST-программы.
Идея доказательства демонстрируется на примере трехсчетчиковой машины Минского, реализующей функцию возведения числа в квадрат.
Ключевые слова:
программируемые логические контроллеры (ПЛК), построение и верификация ПЛК-программ, LTL-спецификация, счётчиковые машины Минского.
Образец цитирования:
Е. В. Кузьмин, Д. А. Рябухин, В. А. Соколов, “О выразительности подхода к построению ПЛК-программ по LTL-спецификации”, Модел. и анализ информ. систем, 22:4 (2015), 507–520
\RBibitem{KuzRyaSok15}
\by Е.~В.~Кузьмин, Д.~А.~Рябухин, В.~А.~Соколов
\paper О выразительности подхода к построению ПЛК-программ по~LTL-спецификации
\jour Модел. и анализ информ. систем
\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://mathscinet.ams.org/mathscinet-getitem?mr=3418470}
\elib{https://elibrary.ru/item.asp?id=24273051}
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/mais456
https://www.mathnet.ru/rus/mais/v22/i4/p507
Эта публикация цитируется в следующих 5 статьяx:
М. В. Нейзов, Е. В. Кузьмин, “LTL-спецификация для разработки и верификации управляющих программ”, Модел. и анализ информ. систем, 30:4 (2023), 308–339
Edisson Eder Caballero Ames, Brayan Jesus Leon Quilca, Elvis Nelson Urbano Taipe, Deyby Maycol Huamanchahua Canchanya, 2022 2nd International Conference on Robotics, Automation and Artificial Intelligence (RAAI), 2022, 272
A. S. Kozodaev, A. V. Nerovnyh, SECOND INTERNATIONAL CONFERENCE ON MATERIAL SCIENCE, SMART STRUCTURES AND APPLICATIONS: ICMSS-2019, 2201, SECOND INTERNATIONAL CONFERENCE ON MATERIAL SCIENCE, SMART STRUCTURES AND APPLICATIONS: ICMSS-2019, 2019, 020046
D. A. Ryabukhin, E. V. Kuzmin, V. A. Sokolov, “Construction of CFC-Programs by LTL-Specification”, Aut. Control Comp. Sci., 51:7 (2017), 567
Д. А. Рябухин, Е. В. Кузьмин, В. А. Соколов, “Построение CFC-программ ПЛК по LTL-спецификации”, Модел. и анализ информ. систем, 23:2 (2016), 173–184
Цитирование в формате AMSBIB
Обратная связь: