Моделирование и анализ информационных систем
RUS  ENG    ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB  
Общая информация
Последний выпуск
Архив
Импакт-фактор

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Моделирование и анализ информационных систем, 2013, том 20, номер 4, страницы 5–22 (Mi mais318)  

Эта публикация цитируется в 6 научных статьях (всего в 6 статьях)

Построение и верификация ПЛК-программ по LTL-спецификации

Е. В. Кузьмин, В. А. Соколов, Д. А. Рябухин

Ярославский государственный университет им. П. Г. Демидова, 150000 Россия, г. Ярославль, ул. Советская, 14
Список литературы:
Аннотация: Предлагается подход к построению и верификации программ логических контроллеров (ПЛК) для «дискретных» задач. Спецификация программного поведения проводится на языке темпоральной логики линейного времени LTL. Программирование осуществляется на языке ST (Structured Text) по LTL-спецификации. Анализ корректности LTL-спецификации производится с помощью программного средства символьной проверки модели Cadence SMV. Предлагаемый подход к программированию и верификации программ ПЛК демонстрируется на примере. Для дискретной задачи приводятся ST-программа, ее LTL-спецификация и SMV-модель.
Целью статьи является описание подхода к программированию ПЛК, который бы обеспечивал возможность анализа корректности ПЛК-программ с помощью метода проверки модели.
Поэтому изменение значения каждой программной переменной описывается с помощью пары LTL-формул. Первая LTL-формула описывает ситуации, при которых происходит возрастание значения соответствующей переменной, вторая LTL-формула задает условия, приводящие к уменьшению значения переменной. Рассматриваемые для спецификации поведения переменных LTL-формулы являются конструктивными в том смысле, что по ним производится построение ПЛК-программы, которая соответствует темпоральным свойствам, выраженным этими формулами. Таким образом, программирование ПЛК сводится к построению LTL-спецификации поведения каждой программной переменной. Кроме этого, по LTL-спецификации строится SMV-модель, которая затем проверяется на корректность (относительно дополнительных общепрограммных LTL-свойств) методом проверки модели с помощью средства верификации Cadence SMV.
Ключевые слова: программируемые логические контроллеры, технология программирования, спецификация и верификация программ.
Поступила в редакцию: 20.05.2013
Тип публикации: Статья
УДК: 517.9
Образец цитирования: Е. В. Кузьмин, В. А. Соколов, Д. А. Рябухин, “Построение и верификация ПЛК-программ по LTL-спецификации”, Модел. и анализ информ. систем, 20:4 (2013), 5–22
Цитирование в формате AMSBIB
\RBibitem{KuzSokRya13}
\by Е.~В.~Кузьмин, В.~А.~Соколов, Д.~А.~Рябухин
\paper Построение и верификация ПЛК-программ по~LTL-спецификации
\jour Модел. и анализ информ. систем
\yr 2013
\vol 20
\issue 4
\pages 5--22
\mathnet{http://mi.mathnet.ru/mais318}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/mais318
  • https://www.mathnet.ru/rus/mais/v20/i4/p5
  • Эта публикация цитируется в следующих 6 статьяx:
    Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Моделирование и анализ информационных систем
     
      Обратная связь:
     Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024