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

 Рис. 1. Структура элементарной EDTL-записи

Предложен событийно-темпоральный способ (event-driven temporal logic pattern, или, сокращенно, EDTL-паттерн) спецификации функциональных требований для реактивных систем (Рис. 1), который сводится к заданию списка шестикомпонентных кортежей. Единичный кортеж (элементарное EDTL-требование) определяется (1) триггерным событием, (2) финализирующим событием, (3) реакцией на триггерное событие, (4) допустимой задержкой на реакцию, (5) инвариантом и (6) событием отмены триггерного события. Получено преобразование элементарной EDTL-записи в утверждения линейной темпоральной логики и логики первого порядка, что доказывает совместимость предлагаемого подхода с существующими системами формальной верификации. Продемонстрирована конструктивность семантики элементарного EDTL-требования через разработанный алгоритм контроля истинности EDTL-записи на ограниченном множестве путей программы. Отработка способа на тестовых примерах показала его универсальность, гибкость и простоту использования, что обуславливает эффективность его применения при групповой разработке реактивных систем широкого класса: централизованных и распределенных систем управления на базе программируемых логических контроллеров, киберфизических систем, приложений Интернета вещей (IoT), в том, числе промышленного (IIoT), встраиваемых систем и др.

Публикации

1. 1. Zyubin V., Anureev I., Garanina N., Staroletov S., Rozov A., Liakh T. (2021) Event-Driven Temporal Logic Pattern for Control Software Requirements Specification. In: Hojjat H., Massink M. (eds) Fundamentals of Software Engineering. FSEN 2021. Lecture Notes in Computer Science, vol 12818. Springer, Cham. https://doi.org/10.1007/978-3-030-89247-0_7.

Разработка методов трансляции процесс-ориентированных программ в Promela-программы

Предложена система переходов гиперпроцессов (HTS) для моделирования программного обеспечения узлов систем промышленного Интернета вещей на базе ПЛК и новая логика cycleLTL для формулирования свойств узла приложения IIoT. Определены правила трансляции формул логики cycle-LTL в формулы логики LTL. Доказана корректность преобразований и, соответственно, разрешимость задачи проверки моделей для HTS и cycle-LTL. Предложен общий подход трансформации Reflex-программ в Promela-модели.

Публикации

1. N. O. Garanina, I. S. Anureev, V. E. Zyubin, S. M. Staroletov, T. V. Liakh, A. S. Rozov, and S. P. Gorlatch. A Temporal Logic for Programmable Logic Controllers. // ISSN 0146-4116, Automatic Control and Computer Sciences, 2021, Vol. 55, No. 7, pp. 763–775. © Allerton Press, Inc., 2021.

2. A. A. Ponomarenko, N. O. Garanina, S. M. Staroletov and V. E. Zyubin, "Towards the Translation of Reflex Programs to Promela: Model Checking Wheelchair Lift Software," 2021 IEEE 22nd International Conference of Young Professionals in Electron Devices and Materials (EDM), 2021, pp. 493-498, https://doi.org/10.1109/EDM52169.2021.9507563