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

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

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



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






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


Модел. и анализ информ. систем, 2014, том 21, номер 4, страницы 75–90 (Mi mais389)  

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

Моделирование согласованного поведения ПЛК-датчиков

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

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

Аннотация: Статья продолжает цикл работ, посвященный разработке подхода к построению и верификации «дискретных» программ логических контроллеров (ПЛК), обеспечивающего возможность анализа их корректности с помощью метода проверки модели (model checking). Подход получил название «Программирование и верификация по LTL-спецификации».
При верификации ПЛК-программы методом проверки модели возникает необходимость в построении ее конечной модели. При этом для успешной проверки соответствия модели требуемым программным свойствам важно учитывать то, что далеко не все комбинации входных сигналов от датчиков могут встречаться в действительности при работе ПЛК с объектом управления. Этот факт требует более внимательного отношения к построению модели программы ПЛК.
В статье предлагается описывать согласованное поведение датчиков с помощью трех групп LTL-формул, которые при проверке справедливости программных свойств будут оказывать влияние на программную модель, приближая ее к реальному поведению исходной ПЛК-программы. Идея LTL-требований демонстрируется на примере.
Программа ПЛК представляет собой описание реакций на входные сигналы от датчиков, переключателей и кнопок. Предложенный подход к моделированию согласованного поведения ПЛК-датчиков при построении модели программы ПЛК позволяет сосредоточиться на моделировании именно этих реакций по тексту программы без внедрения в код модели дополнительных конструкций, призванных отразить реалистичное поведение датчиков. Согласованное поведение датчиков учитывается лишь на стадии проверки соответствия программной модели требуемым свойствам, т. е. доказательство выполнимости свойств для построенной модели происходит с условием, что рассматриваемая модель содержит только те исполнения исходной программы, которые отвечают требованиям согласованного поведения датчиков.

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

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

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

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


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

    ОТПРАВИТЬ: 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-спецификации”, Модел. и анализ информ. систем, 22:4 (2015), 507–520  mathnet  crossref  mathscinet  elib
    2. Д. А. Рябухин, Е. В. Кузьмин, В. А. Соколов, “Построение CFC-программ ПЛК по LTL-спецификации”, Модел. и анализ информ. систем, 23:2 (2016), 173–184  mathnet  crossref  mathscinet  elib
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:185
    Полный текст:61
    Литература:33
     
    Обратная связь:
     Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2021