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

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

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



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






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


Модел. и анализ информ. систем, 2016, том 23, номер 2, страницы 173–184 (Mi mais489)  

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

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

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

Аннотация: Статья продолжает серию работ, посвященных подходу к построению и верификации «дискретных» программ логических контроллеров (ПЛК) по LTL-спецификации. Этот подход обеспечивает возможность анализа корректности программ логических контроллеров с помощью метода проверки модели (Model Checking). В рамках подхода в качестве языка спецификации программного поведения используется язык темпоральной логики LTL. Анализ корректности LTL-спецификации относительно программных свойств производится автоматически с помощью программного средства символьной проверки модели Cadence SMV.
Ранее было показано, каким образом по корректной (проверенной на корректность относительно программных свойств) LTL-спецификации происходит построение ST-, LD- и IL-программ. В этой статье описывается технология построения CFC-программ по LTL-спецификации. Язык непрерывных функциональных схем CFC (Continuous Function Chart) представляет собой разновидность языка FBD (Function Block Diagram) — графического языка диаграмм принципиальных схем электронных устройств на микросхемах. В отличие от FBD язык CFC обеспечивает возможность свободного размещения программных компонентов и их соединений на экране. Технология построения CFC-программ демонстрируется на примере.
Представление ПЛК-программы на языке CFC в рамках подхода к программированию по LTL-спецификации в отличие от представлений на других стандартных языках дает возможность наглядного графического изображения потока данных от входных переменных к выходам ПЛК. Явным образом демонстрируется зависимость и влияние значений одних переменных на значения других переменных во время исполнения программы за один проход рабочего цикла ПЛК. Фактически CFC-программа представляет собой схему потоков данных ПЛК-программы.

Ключевые слова: программируемые логические контроллеры (ПЛК), построение и верификация ПЛК-программ, LTL-спецификация, CFC-диаграммы.

Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 12-01-00281_a
Работа проводилась при финансовой поддержке РФФИ, грант №12-01-00281-a.


DOI: https://doi.org/10.18255/1818-1015-2016-2-173-184

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

Реферативные базы данных:

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

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

Цитирование в формате AMSBIB
\RBibitem{RyaKuzSok16}
\by Д.~А.~Рябухин, Е.~В.~Кузьмин, В.~А.~Соколов
\paper Построение CFC-программ ПЛК по~LTL-спецификации
\jour Модел. и анализ информ. систем
\yr 2016
\vol 23
\issue 2
\pages 173--184
\mathnet{http://mi.mathnet.ru/mais489}
\crossref{https://doi.org/10.18255/1818-1015-2016-2-173-184}
\mathscinet{http://www.ams.org/mathscinet-getitem?mr=3504587}
\elib{https://elibrary.ru/item.asp?id=25810350}


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

    ОТПРАВИТЬ: 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
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:342
    Полный текст:264
    Литература:40
     
    Обратная связь:
     Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2021