|
Эта публикация цитируется в 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.
Поступила в редакцию: 06.11.2023 Исправленный вариант: 20.11.2023 Принята в печать: 22.11.2023
Образец цитирования:
М. В. Нейзов, Е. В. Кузьмин, “LTL-спецификация для разработки и верификации управляющих программ”, Модел. и анализ информ. систем, 30:4 (2023), 308–339
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/mais806 https://www.mathnet.ru/rus/mais/v30/i4/p308
|
Статистика просмотров: |
Страница аннотации: | 48 | PDF полного текста: | 12 | Список литературы: | 11 |
|