Аннотация:
Статья продолжает серию работ, посвященных подходу к построению и верификации «дискретных» программ логических контроллеров (ПЛК) по LTL-спецификации. Этот подход обеспечивает возможность анализа корректности программ логических контроллеров с помощью метода проверки модели (Model Checking). В рамках подхода в качестве языка спецификации программного поведения используется язык темпоральной логики LTL. Анализ корректности LTL-спецификации относительно программных свойств производится автоматически с помощью программного средства символьной проверки модели Cadence SMV.
Ранее было показано, каким образом по корректной (проверенной на корректность относительно программных свойств) LTL-спецификации происходит построение ST-, LD- и IL-программ. В этой статье описывается технология построения CFC-программ по LTL-спецификации. Язык непрерывных функциональных схем CFC (Continuous Function Chart) представляет собой разновидность языка FBD (Function Block Diagram) — графического языка диаграмм принципиальных схем электронных устройств на микросхемах. В отличие от FBD язык CFC обеспечивает возможность свободного размещения программных компонентов и их соединений на экране. Технология построения CFC-программ демонстрируется на примере.
Представление ПЛК-программы на языке CFC в рамках подхода к программированию по LTL-спецификации в отличие от представлений на других стандартных языках дает возможность наглядного графического изображения потока данных от входных переменных к выходам ПЛК. Явным образом демонстрируется зависимость и влияние значений одних переменных на значения других переменных во время исполнения программы за один проход рабочего цикла ПЛК. Фактически CFC-программа представляет собой схему потоков данных ПЛК-программы.
Работа проводилась при финансовой поддержке РФФИ, грант №12-01-00281-a.
Поступила в редакцию: 01.03.2016
Реферативные базы данных:
Тип публикации:
Статья
УДК:
517.9
Образец цитирования:
Д. А. Рябухин, Е. В. Кузьмин, В. А. Соколов, “Построение CFC-программ ПЛК по LTL-спецификации”, Модел. и анализ информ. систем, 23:2 (2016), 173–184
\RBibitem{RyaKuzSok16}
\by Д.~А.~Рябухин, Е.~В.~Кузьмин, В.~А.~Соколов
\paper Построение CFC-программ ПЛК по~LTL-спецификации
\jour Модел. и анализ информ. систем
\yr 2016
\vol 23
\issue 2
\pages 173--184
\mathnet{http://mi.mathnet.ru/mais489}
\crossref{https://doi.org/10.18255/1818-1015-2016-2-173-184}
\mathscinet{http://mathscinet.ams.org/mathscinet-getitem?mr=3504587}
\elib{https://elibrary.ru/item.asp?id=25810350}
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/mais489
https://www.mathnet.ru/rus/mais/v23/i2/p173
Эта публикация цитируется в следующих 1 статьяx:
М. В. Нейзов, Е. В. Кузьмин, “LTL-спецификация для разработки и верификации управляющих программ”, Модел. и анализ информ. систем, 30:4 (2023), 308–339
Цитирование в формате AMSBIB
Обратная связь: