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

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

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



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






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


Модел. и анализ информ. систем, 2013, том 20, номер 2, страницы 104–120 (Mi mais301)  

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

Моделирование, спецификация и построение программ логических контроллеров

Е. В. Кузьмин, В. А. Соколов

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

Аннотация: Предлагается новый подход к построению надежных «дискретных» ПЛК-программ с таймерами — программирование исходя из задач спецификации и верификации. Для спецификации программного поведения используется язык темпоральной логики LTL. Программирование осуществляется на языке ST по LTL-спецификации. Проводится дискретное моделирование таймера. Новый подход к программированию ПЛК демонстрируется на примере.
Предлагаемый подход к программированию ПЛК обеспечивает возможность анализа корректности ПЛК-программ с помощью метода проверки модели. При программировании требуется соблюдение следующих двух условий: 1) значение каждой переменной должно изменяться не более одного раза за одно полное выполнение программы при прохождении рабочего цикла ПЛК; 2) значение каждой переменной должно изменяться только в одном месте программы ПЛК.
В рамках предлагаемого подхода изменение значения каждой программной переменной описывается с помощью пары LTL-формул. Первая LTL-формула описывает ситуации, при которых происходит возрастание значения соответствующей переменной, вторая LTL-формула задает условия, приводящие к уменьшению значения переменной. Рассматриваемые для спецификации поведения переменных LTL-формулы являются конструктивными в том смысле, что по ним производится построение ПЛК-программы, которая соответствует темпоральным свойствам, выраженным этими формулами. Таким образом, программирование ПЛК сводится к построению LTL-спецификации поведения каждой программной переменной.

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

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

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

Образец цитирования: Е. В. Кузьмин, В. А. Соколов, “Моделирование, спецификация и построение программ логических контроллеров”, Модел. и анализ информ. систем, 20:2 (2013), 104–120

Цитирование в формате AMSBIB
\RBibitem{KuzSok13}
\by Е.~В.~Кузьмин, В.~А.~Соколов
\paper Моделирование, спецификация и построение программ логических контроллеров
\jour Модел. и анализ информ. систем
\yr 2013
\vol 20
\issue 2
\pages 104--120
\mathnet{http://mi.mathnet.ru/mais301}


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

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

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