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

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

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



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






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


Модел. и анализ информ. систем, 2014, том 21, номер 2, страницы 26–38 (Mi mais368)  

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

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

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

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

Аннотация: Предлагается подход к построению и верификации IL-программ логических контроллеров (ПЛК) для «дискретных» задач. Спецификация программного поведения проводится на языке темпоральной логики линейного времени LTL. Программирование осуществляется на языке IL (Instruction List) по LTL-спецификации. Анализ корректности LTL-спецификации производится с помощью программного средства символьной проверки модели Cadence SMV. Подход к программированию и верификации IL-программ ПЛК демонстрируется на примере. Для дискретной задачи приводятся IL-программа и ее LTL-спецификация.
Целью статьи является описание подхода к программированию ПЛК, который бы обеспечивал возможность анализа корректности IL-программ ПЛК с помощью метода проверки модели.
Поэтому изменение значения каждой программной переменной описывается с помощью пары LTL-формул. Первая LTL-формула описывает ситуации, при которых происходит возрастание значения соответствующей переменной, вторая LTL-формула задает условия, приводящие к уменьшению значения переменной. Рассматриваемые для спецификации поведения переменных LTL-формулы являются конструктивными в том смысле, что по ним производится построение ПЛК-программы, которая соответствует темпоральным свойствам, выраженным этими формулами. Таким образом, программирование ПЛК сводится к построению LTL-спецификации поведения каждой программной переменной. Кроме этого, по LTL-спецификации строится SMV-модель IL-программы ПЛК, которая затем проверяется на корректность (относительно дополнительных общепрограммных LTL-свойств) методом проверки модели с помощью средства верификации Cadence SMV.

Ключевые слова: программируемые логические контроллеры, технология программирования, спецификация и верификация программ, список инструкций.

Полный текст: PDF файл (181 kB)
Список литературы: PDF файл   HTML файл
Тип публикации: Статья
УДК: 517.9
Поступила в редакцию: 03.02.2014

Образец цитирования: Д. А. Рябухин, Е. В. Кузьмин, В. А. Соколов, “Построение IL-программ ПЛК по LTL-спецификации”, Модел. и анализ информ. систем, 21:2 (2014), 26–38

Цитирование в формате AMSBIB
\RBibitem{RyaKuzSok14}
\by Д.~А.~Рябухин, Е.~В.~Кузьмин, В.~А.~Соколов
\paper Построение IL-программ ПЛК по~LTL-спецификации
\jour Модел. и анализ информ. систем
\yr 2014
\vol 21
\issue 2
\pages 26--38
\mathnet{http://mi.mathnet.ru/mais368}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais368
  • http://mi.mathnet.ru/rus/mais/v21/i2/p26

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles

    Эта публикация цитируется в следующих статьяx:
    1. Е. В. Кузьмин, Д. А. Рябухин, В. А. Соколов, “Моделирование согласованного поведения ПЛК-датчиков”, Модел. и анализ информ. систем, 21:4 (2014), 75–90  mathnet
    2. Е. В. Кузьмин, Д. А. Рябухин, В. А. Соколов, “О выразительности подхода к построению ПЛК-программ по LTL-спецификации”, Модел. и анализ информ. систем, 22:4 (2015), 507–520  mathnet  crossref  mathscinet  elib
    3. Д. А. Рябухин, Е. В. Кузьмин, В. А. Соколов, “Построение CFC-программ ПЛК по LTL-спецификации”, Модел. и анализ информ. систем, 23:2 (2016), 173–184  mathnet  crossref  mathscinet  elib
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:380
    Полный текст:257
    Литература:40
     
    Обратная связь:
     Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2021