ISSN 1818-1015 · EISSN 2313-5417

Язык: ru

Статья: LTL-СПЕЦИФИКАЦИЯ ДЛЯ РАЗРАБОТКИ И ВЕРИФИКАЦИИ УПРАВЛЯЮЩИХ ПРОГРАММ (2023)

Читать

Читать онлайн

Настоящая работа продолжает цикл статей по разработке и верификации управляющих программ на основе LTL“=спецификации. Суть подхода заключается в описании поведения программ с помощью формул линейной темпоральной логики LTL специального вида. Полученная LTL“=спецификация может быть непосредственно верифицирована с помощью инструмента проверки модели. Далее по LTL“=спецификации однозначно строится код программы на императивном языке программирования. Перевод спецификации в программу осуществляется по шаблону. Новизна работы состоит в предложении двух LTL“=спецификаций нового вида - декларативной и императивной, а также в более строгом формальном обосновании данного подхода к разработке и верификации программ. Выполнен переход на более современный инструмент верификации конечных и бесконечных систем - nuXmv. Предлагается описывать поведение управляющих программ в декларативном стиле. Для этого предназначена декларативная LTL“=спецификация, которая задаёт размеченную систему переходов как формальную модель поведения программы. Данный способ описания поведения является достаточно выразительным - доказана теорема о Тьюринг“=полноте декларативной LTL“=спецификации. Далее для построения кода программы на императивном языке декларативная LTL“=спецификация преобразуется в эквивалентную императивную LTL“=спецификацию. Доказана теорема об эквивалентности, которая гарантирует, что обе спецификации задают одно и то же поведение. Императивная LTL“=спецификация транслируется в императивный код программы по представленному шаблону. Декларативная LTL“=спецификация, которая подвергается верификации, и построенная по ней управляющая программа гарантированно задают одно и то же поведение в виде соответствующей системы переходов. Таким образом, при верификации используется модель, адекватная реальному поведению управляющей программы.

Ключевые фразы: УПРАВЛЯЮЩЕЕ ПРОГРАММНОЕ ОБЕСПЕЧЕНИЕ, ДЕКЛАРАТИВНАЯ LTL-СПЕЦИФИКАЦИЯ, ИМПЕРАТИВНАЯ LTL-СПЕЦИФИКАЦИЯ, ПОЛНАЯ СИСТЕМА ПЕРЕХОДОВ, ПСЕВДОПОЛНАЯ СИСТЕМА ПЕРЕХОДОВ, СЧЁТЧИКОВАЯ МАШИНА МИНСКОГО, ПРОВЕРКА МОДЕЛИ, ВЕРИФИКАТОР NUXMV, ПЛК-ПРОГРАММА, ЯЗЫК ST

Автор (ы): Нейзов Максим Вячеславович, Кузьмин Егор Владимирович

Журнал: МОДЕЛИРОВАНИЕ И АНАЛИЗ ИНФОРМАЦИОННЫХ СИСТЕМ

Идентификаторы и классификаторы

УДК: 004.424. Методы программирования
519.683.8. Специальные приемы программирования
eLIBRARY ID: 54949252

Для цитирования:

НЕЙЗОВ М. В., КУЗЬМИН Е. В. LTL-СПЕЦИФИКАЦИЯ ДЛЯ РАЗРАБОТКИ И ВЕРИФИКАЦИИ УПРАВЛЯЮЩИХ ПРОГРАММ // МОДЕЛИРОВАНИЕ И АНАЛИЗ ИНФОРМАЦИОННЫХ СИСТЕМ. 2023. Т. 30 № 4

Текстовый фрагмент статьи

При решении задач управления проектируемая система естественным образом разделяется на систему управления и объект управления, оказывающие влияние друг на друга в процессе работы. Программное обеспечение (ПО), реализующее процесс управления, является управляющим ПО (УПО) и представляет собой систему управления или её часть. Объект управления может иметь различную природу и назначение. Например, в киберфизической системе [1, 2] УПО формирует воздействие на физическую среду, взаимодействуя с ней через сенсоры и исполнительные устройства. Так программа программируемого логического контроллера (ПЛК) [3] управляет технологическим процессом на производстве. В этом случае УПО является частью аппаратно-программной системы управления. Другой пример — в системе управления базами данных УПО выполняет различные манипуляции с массивом данных, осуществляя управление их выборкой и хранением.

Здесь объектом управления является массив данных, который имеет не физическую, а программную природу, как и система управления. При решении же вычислительных задач проектируемая система содержит только программные компоненты. Согласно [4] дискретный преобразователь информации может быть представлен в виде автоматной модели, состоящей из взаимодействующих компонентов — операционного и управляющего автоматов. Операционный автомат преобразует информацию, а управляющий автомат осуществляет управление действиями по её преобразованию, т. е. описывает процесс управления вычислениями. Выделение задачи управления при разработке ПО присуще направлению, которое получило название программная кибернетика [5]. В рамках этого подхода управляющий и операционный автоматы могут быть реализованы в виде программных компонентов на любом уровне абстракции, который определяется решаемой задачей [6]. Таким образом, УПО может разрабатываться как отдельная часть проектируемой системы при решении не только управляющих, но и вычислительных задач.

Список литературы

S. Oks, M. Jalowski, M. Lechner, and others, “Cyber-Physical Systems in the Context of Industry 4.0: A Review, Categorization and Outlook”, Inf. Systems Frontiers, 2022,. DOI: 10.1007/s10796-022-10252-x
E. A. Lee and S. A. Seshia, Introduction to Embedded Systems - A Cyber-Physical Systems Approach, 2nd ed. MIT Press, 2017.
E. A. Parr, Programmable Controllers. An Engineer’s Guide, 3rd ed. Newnes, 2003.
V. N. Lifshic and L. E. Sadovskii, “Algebraic Models of Computing Machines”, UMN, vol. 27, no. 3(165), pp. 79-125, 1972.
K.-Y. Cai, T. Y. Chen, and T. H. Tse, “Towards Research on Software Cybernetics”, in Proceedings of 7th IEEE International on High-assurance Systems Engineering (HASE 2002), 2002, pp. 240-241.
N. I. Polikarpova and A. A. Shalyto, Automata-Based Programming, 2nd ed. Spb.: Piter, 2011.
D. Harel and A. Pnueli, “On the Development of Reactive Systems”, in Logics and Models of Concurrent Systems, 1985, vol. 13, pp. 477-498.
A. Pnueli, “Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A Survey of Current Trends”, in Current Trends in Concurrency, 1986, vol. 224, pp. 510-584.
A. Maurya and D. Kumar, “Reliability of safety-critical systems: A state-of-the-art review”, Quality and Reliability Engineering International, vol. 36, no. 7, pp. 2547-2568, 2020.

N. Rajabli, F. Flammini, R. Nardone, and V. Vittorini, "Software Verification and Validation of Safe Autonomous Cars: A Systematic Literature Review", in IEEE Access, 2021, vol. 9, pp. 4797-4819.

V. D'Silva, D. Kroening, and G. Weissenbacher, "A Survey of Automated Techniques for Formal Software Verification", in IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2008, vol. 27, no. 7, pp. 1165-1178.

E. M. Clarke, T. A. Henzinger, H. Veith, and R. Bloem, Handbook of Model Checking, 1st ed. Springer Publishing Company, Incorporated, 2018.

Y. G. Karpov, Model checking. Verification of Parallel and Distributed Program Systems. BHV-Peterburg, 2010.

S. Velder, M. Lukin, A. Shalyto, and B. Yaminov, Verification of Automata-Based Programs. Spb Science, 2011.

E. M. Clarke, O. Grumberg, and D. Peled, Verification of Program Models: Model Checking. MCNMO, 2002.

E. V. Kuzmin and V. A. Sokolov, "Modeling, Specification and Construction of PLC-programs", Modeling and Analysis of Information Systems, vol. 20, no. 2, pp. 104-120, 2013.  EDN: QLSCBV

E. V. Kuzmin and V. A. Sokolov, "Modeling, Specification and Construction of PLC-programs", Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 554-563, 2014.  EDN: XFFXBH

E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, "Construction and Verification of PLC-programs by LTL-specification", Modeling and Analysis of Information Systems, vol. 20, no. 4, pp. 5-22, 2013.  EDN: RHITBR

E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, "Construction and Verification of PLC-Programs by LTL-Specification", Automatic Control and Computer Sciences, vol. 49, no. 7, pp. 453-465, 2015.  EDN: WPQTYX

E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, "Construction and Verification of PLC LD-programs by LTL-specification", Modeling and Analysis of Information Systems, vol. 20, no. 6, pp. 78-94, 2013.  EDN: SLAOHT

E. V. Kuzmin, V. A. Sokolov, and D. A. Ryabukhin, "Construction and Verification of PLC LD Programs by the LTL Specification", Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 424-436, 2014.  EDN: WVVYBP

D. A. Ryabukhin, E. V. Kuzmin, and V. A. Sokolov, "Construction of PLC IL-programs by LTL-specification", Modeling and Analysis of Information Systems, vol. 21, no. 2, pp. 26-38, 2014.  EDN: SEDRNT

E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, "Modeling a Consistent Behavior of PLC-Sensors", Modeling and Analysis of Information Systems, vol. 21, no. 4, pp. 75-90, 2014.  EDN: SVJRWR

E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, "Modeling a Consistent Behavior of PLC-Sensors", Automatic Control and Computer Sciences, vol. 48, no. 7, pp. 602-614, 2014.  EDN: WVVWCL

E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, "On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification", Modeling and Analysis of Information Systems, vol. 22, no. 4, pp. 507-520, 2015.  EDN: ULEIUV

E. V. Kuzmin, D. A. Ryabukhin, and V. A. Sokolov, "On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification", Automatic Control and Computer Sciences, vol. 50, pp. 510-519, 2016.

D. A. Ryabukhin, E. V. Kuzmin, and V. A. Sokolov, "Construction of CFC-programs by LTL-specification", Modeling and Analysis of Information Systems, vol. 23, no. 2, pp. 173-184, 2016.  EDN: RJVZYD

D. A. Ryabukhin, E. V. Kuzmin, and V. A. Sokolov, "Construction of CFC-Programs by LTL-Specification", Automatic Control and Computer Sciences, vol. 51, pp. 567-575, 2017.

E. V. Kuzmin, "LTL-Specification of Counter Machines", Modeling and Analysis of Information Systems, vol. 28, no. 1, pp. 104-119, 2021.  EDN: XHKKKU

E. V. Kuzmin, "LTL-Specification of Bounded Counter Machines", Modeling and Analysis of Information Systems, vol. 29, no. 1, pp. 44-59, 2022.  EDN: OAPYWT

E. V. Kuzmin and V. A. Sokolov, "On Construction and Verification of PLC-Programs", Modeling and Analysis of Information Systems, vol. 19, no. 4, pp. 25-36, 2012.  EDN: PIXSGT

E. V. Kuzmin and V. A. Sokolov, "On Construction and Verification of PLC Programs", Automatic Control and Computer Sciences, vol. 47, no. 7, pp. 443-451, 2013.  EDN: SLNKTN

"IEC 61131-3:2013 Programmable controllers - Part 3: Programming languages". [Online]. Available: https://webstore.iec.ch/publication/4552.

A. Pnueli, "The Temporal Logic of Programs", in 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), 1977, pp. 46-57.

M. L. Minsky, Computation: Finite and Infinite Machines. Prentice-Hall, 1967.

R. Schroeppel, "A Two Counter Machine Cannot Calculate 2ᴺ", Massachusetts Institute of Technology, Artificial Intelligence Laboratory, Artificial Intelligence Memo #257, 1972.

E. V. Kuzmin, Counter Machines. Yaroslavl State University, 2010.

Выпуск

Т. 30 № 4 (2023)

Кол-во страниц: 140 страниц

Другие статьи выпуска

АЛГОРИТМ ПРЕДСКАЗАНИЯ СВЯЗЕЙ В САМОРЕГУЛИРУЮЩЕЙСЯ СЕТИ С АДАПТИВНОЙ ТОПОЛОГИЕЙ НА БАЗЕ ТЕОРИИ ГРАФОВ И МАШИННОГО ОБУЧЕНИЯ (2023)

Авторы: Павленко Евгений Юрьевич

В статье представлена графовая модель функционирования сети с адаптивной топологией, где узлы сети представляют собой вершины графа, а обмен данными между узлами представлен в виде ребер. Динамический характер сетевого взаимодействия осложняет решение задачи мониторинга и контроля функционирования сети с адаптивной топологией, которую необходимо выполнять для обеспечения гарантированно корректного сетевого взаимодействия. Значимость решения такой задачи обосновывается созданием современных информационных и киберфизических систем, в основе которых лежат сети с адаптивной топологией. Динамический характер связей между узлами, с одной стороны, позволяет обеспечивать саморегуляцию сети, с другой стороны, существенно осложняет контроль за работой сети в связи с невозможностью выделения единого шаблона сетевого взаимодействия. На базе разработанной модели функционирования сети с адаптивной топологией предложен графовый алгоритм предсказания связей, распространенный на случай с одноранговыми сетями. В основу алгоритма положены значимые параметры узлов сети, харатеризующие как их физические характеристики (уровень сигнала, заряд батареи), так и их характеристики как объектов сетевого взаимодействия (характеристики центральности вершин графа). Корректность и адекватность разработанного алгоритма подтверждена экспериментальными результатами по моделированию одноранговой сети с адаптивной топологией и ее саморегуляции при удалении различных узлов.

Сохранить в закладках

Издательство

Издательство: ЯрГУ им. П.Г. Демидова
Регион: Россия, Ярославль
Почтовый адрес: 150003, Ярославль, Советская, 14,
Юр. адрес: 150003, Ярославль, Советская, 14,
ФИО: Иванчин Артем Владимирович (Ректор)
E-mail адрес: rectorat@uniyar.ac.ru
Контактный телефон: +7 (485) 2797702
Сайт: https://www.uniyar.ac.ru/

Все права на тексты и товарные знаки принадлежат их законным владельцам. Подробнее...

Сайт https://scinetwork.ru (далее – сайт) работает по принципу агрегатора – собирает и структурирует информацию из публичных источников в сети Интернет, то есть передает полнотекстовую информацию о товарных знаках в том виде, в котором она содержится в открытом доступе.

Сайт и администрация сайта не используют отображаемые на сайте товарные знаки в коммерческих и рекламных целях, не декларируют своего участия в процессе их государственной регистрации, не заявляют о своих исключительных правах на товарные знаки, а также не гарантируют точность, полноту и достоверность информации.

Все права на товарные знаки принадлежат их законным владельцам!

Сайт носит исключительно информационный характер, и предоставляемые им сведения являются открытыми публичными данными.

Администрация сайта не несет ответственность за какие бы то ни было убытки, возникающие в результате доступа и использования сайта.

Спасибо, понятно.