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

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

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



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






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


Моделирование и анализ информационных систем, 2023, том 30, номер 4, страницы 308–339
DOI: https://doi.org/10.18255/1818-1015-2023-4-308-339
(Mi mais806)
 

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

Theory of software

LTL-спецификация для разработки и верификации управляющих программ

М. В. Нейзовa, Е. В. Кузьминb

a Институт автоматики и электрометрии СО РАН, просп. Академика Коптюга, д. 1, г. Новосибирск, 630090 Россия
b Ярославский государственный университет им. П.Г. Демидова, ул. Советская, д. 14, г. Ярославль, 150003 Россия
Список литературы:
Аннотация: Настоящая работа продолжает цикл статей по разработке и верификации управляющих программ на основе LTL-спецификации. Суть подхода заключается в описании поведения программ с помощью формул линейной темпоральной логики LTL специального вида. Полученная LTL-спецификация может быть непосредственно верифицирована с помощью инструмента проверки модели. Далее по LTL-спецификации однозначно строится код программы на императивном языке программирования. Перевод спецификации в программу осуществляется по шаблону.
Новизна работы состоит в предложении двух LTL-спецификаций нового вида — декларативной и императивной, а также в более строгом формальном обосновании данного подхода к разработке и верификации программ. Выполнен переход на более современный инструмент верификации конечных и бесконечных систем — nuXmv. Предлагается описывать поведение управляющих программ в декларативном стиле. Для этого предназначена декларативная LTL-спецификация, которая задаёт размеченную систему переходов как формальную модель поведения программы. Данный способ описания поведения является достаточно выразительным — доказана теорема о Тьюринг-полноте декларативной LTL-спецификации. Далее для построения кода программы на императивном языке декларативная LTL-спецификация преобразуется в эквивалентную императивную LTL-спецификацию. Доказана теорема об эквивалентности, которая гарантирует, что обе спецификации задают одно и то же поведение. Императивная LTL-спецификация транслируется в императивный код программы по представленному шаблону. Декларативная LTL-спецификация, которая подвергается верификации, и построенная по ней управляющая программа гарантированно задают одно и то же поведение в виде соответствующей системы переходов. Таким образом, при верификации используется модель, адекватная реальному поведению управляющей программы.
Ключевые слова: управляющее программное обеспечение, декларативная LTL-спецификация, императивная LTL-спецификация, полная система переходов, псевдополная система переходов, счётчиковая машина Минского, проверка модели, верификатор nuXmv, ПЛК-программа, язык ST.
Финансовая поддержка Номер гранта
Министерство науки и высшего образования Российской Федерации 122031600173-8
Ярославский государственный университет VIP-016
Госзадание ИАиЭ СО РАН, проект № 122031600173-8; ЯрГУ (проект VIP-016).
Поступила в редакцию: 06.11.2023
Исправленный вариант: 20.11.2023
Принята в печать: 22.11.2023
Тип публикации: Статья
УДК: 004.424+519.683.8
MSC: 68N30
Образец цитирования: М. В. Нейзов, Е. В. Кузьмин, “LTL-спецификация для разработки и верификации управляющих программ”, Модел. и анализ информ. систем, 30:4 (2023), 308–339
Цитирование в формате AMSBIB
\RBibitem{NeyKuz23}
\by М.~В.~Нейзов, Е.~В.~Кузьмин
\paper LTL-спецификация для разработки и верификации управляющих программ
\jour Модел. и анализ информ. систем
\yr 2023
\vol 30
\issue 4
\pages 308--339
\mathnet{http://mi.mathnet.ru/mais806}
\crossref{https://doi.org/10.18255/1818-1015-2023-4-308-339}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/mais806
  • https://www.mathnet.ru/rus/mais/v30/i4/p308
  • Эта публикация цитируется в следующих 2 статьяx:
    Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Моделирование и анализ информационных систем
    Статистика просмотров:
    Страница аннотации:48
    PDF полного текста:12
    Список литературы:11
     
      Обратная связь:
     Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024