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

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

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



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






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


Модел. и анализ информ. систем, 2013, том 20, номер 6, страницы 78–94 (Mi mais344)  

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

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

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

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

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

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

Полный текст: PDF файл (249 kB)
Список литературы: PDF файл   HTML файл

Тип публикации: Статья
УДК: 517.9
Поступила в редакцию: 28.10.2013

Образец цитирования: Е. В. Кузьмин, В. А. Соколов, Д. А. Рябухин, “Построение и верификация LD-программ ПЛК по LTL-спецификации”, Модел. и анализ информ. систем, 20:6 (2013), 78–94

Цитирование в формате AMSBIB
\RBibitem{KuzSokRya13}
\by Е.~В.~Кузьмин, В.~А.~Соколов, Д.~А.~Рябухин
\paper Построение и верификация LD-программ ПЛК по LTL-спецификации
\jour Модел. и анализ информ. систем
\yr 2013
\vol 20
\issue 6
\pages 78--94
\mathnet{http://mi.mathnet.ru/mais344}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais344
  • http://mi.mathnet.ru/rus/mais/v20/i6/p78

    ОТПРАВИТЬ: 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. Д. А. Рябухин, Е. В. Кузьмин, В. А. Соколов, “Построение IL-программ ПЛК по LTL-спецификации”, Модел. и анализ информ. систем, 21:2 (2014), 26–38  mathnet
    2. Е. В. Кузьмин, Д. А. Рябухин, В. А. Соколов, “Моделирование согласованного поведения ПЛК-датчиков”, Модел. и анализ информ. систем, 21:4 (2014), 75–90  mathnet
    3. Е. В. Кузьмин, Д. А. Рябухин, В. А. Соколов, “О выразительности подхода к построению ПЛК-программ по LTL-спецификации”, Модел. и анализ информ. систем, 22:4 (2015), 507–520  mathnet  crossref  mathscinet  elib
    4. Д. А. Рябухин, Е. В. Кузьмин, В. А. Соколов, “Построение CFC-программ ПЛК по LTL-спецификации”, Модел. и анализ информ. систем, 23:2 (2016), 173–184  mathnet  crossref  mathscinet  elib
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:353
    Полный текст:72
    Литература:28

     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019