popCAN – протокол прикладного уровня для организации межузлового взаимодействия в распределенных системах процесс-ориентированного управления

 Рис. 1. Концепция popCAN: коммуникационный модуль, периферийные модули, идентификация сообщений.

На основе проведенного анализа модельных и практических задач предложен протокол прикладного уровня popCAN, который задает алгоритмы идентификации узлов и межузловых коммуникаций, удаленного запуска процессов, позволяет подключать до 125 периферийных узлов, обеспечивает организацию p2p-соединений (до 7), реализует возможность подключения неинициализированных модулей, загрузки модулей, передачи длинных сообщений (1 Кбайт) со скоростью 1 Мбит/с. Разработанный протокол упрощает создание распределенных систем управления микроконтроллерами на основе процессно-ориентированной парадигмы программирования.

Публикации

1. V. Zyubin, "popCAN: CAN-bus Application Level Protocol for Implementing Inter-Process Communication in Distributed Microcontroller Systems," 2024 IEEE International Multi-Conference on Engineering, Computer and Information Sciences (SIBIRCON), Novosibirsk, Russian Federation, 2024, pp. 462-466, doi: 10.1109/SIBIRCON63777.2024.10758506. 

Исследование алгоритмов детекции событий в условиях жестких режимов функционирования КФС

 Рис. Автомат состояний сервопривода

Для задачи детекции событий в КФС следящего привода с ШИМ контроллером:
построен односторонний алгоритм асимптотической детекции с учетом динамики событийной функции с негладкими границами проведены вычислительные эксперименты в окружении передовых отечественных (ИСМА, SimInTech) и зарубежных (MATLAB/Simulink, PTOLEMY) инструментальных средств с анализом результатов исследований. Численные эксперименты с программными моделями, представленными в виде карты поведения, показали качественно одинаковые результаты. При этом доказано, что только предложенный алгоритм асимптотической детекции обеспечивает выполнение принципа односторонности событий. Алгоритм встроен в библиотеку явных методов с контролем устойчивости для жестких задач в отечественную инструментальную среду моделирования ИСМА.

Публикации

1. Шорников Ю. В., Тимофеев К. А., Филимонов М.О. Инструментальное моделирование гибридной системы маятника с отрывом // Системы анализа и обработки данных = Analysis and data processing systems. – 2025. – № 4 (100).

Конструктивный метод разрешения конфликтов множественного доступа в процесс-ориентированных программа

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

При экспериментальной апробации метода на модельной программе управления установкой по выращиванию монокристаллов кремния методом Чохральского было получено радикальное сокращение степени недетерминизма (на 98%). При этом, обнаружено, что случай сохранения недетерминизма после модификации вызван ошибкой в дизайне программы. Предлагаемая модификация является эффективным механизмом разрешения конфликтов множественного доступа в процесс ориентированных программах, который либо приводит к разрешению конфликта, либо указывает на наличие ошибки в программе и необходимость ее рефакторинга.

Публикации

1. Д.А. Пермяшкин, В.Е. Зюбин КОНСТРУКТИВНЫЙ МЕТОД РАЗРЕШЕНИЯ КОНФЛИКТОВ МНОЖЕСТВЕННОГО ДОСТУПА В ПРОЦЕСС-ОРИЕНТИРОВАННЫХ ПРОГРАММАХ. -- Автометрия. 2025. Т. 61. №5. С.73-80. DOI: 10.15372/AUT20250509

Способ спецификации узлов микроконтроллерных киберфизических систем

 Рис. Фрагмент кода со спецификацией узлов

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

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

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

Разработка генератора условий корректности для Reflex-программ

 Рис. Схема генерации условий корректности

Разработана трансляционная семантика аннотированных программ на предметно-ориентированном языке конечно-автоматного моделирования КФС Reflex во входной язык Isar системы Isabelle/HOL и на ее основе реализована новая версия генератора условий корректности Reflex-программ (системы логических утверждений, представляющих программу).

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

Также в трансляционную семантику (и в генератор условий корректности) языка Reflex были включены операторы легковесных состояний slice и wait. Генератор условий корректности реализован на языке java и ANTLR 4.0.

Публикации

1. A. D. Ishchenko and I. S. Anureev, "Verification Condition Generator for Revised Reflex Language Using Isabelle/HOL," 2025 IEEE 26th International Conference of Young Professionals in Electron Devices and Materials (EDM), Altai, Russian Federation, 2025, pp. 1440-1445, doi: 10.1109/EDM65517.2025.11096836.

Разработка генератора теории Isabelle/HOL для poST-программ

 Рис. Схема генерации теории Isabelle/HOL для poST-программ

Разработана трансляционная семантика аннотированных программ на предметно-ориентированном языке конечно-автоматного моделирования КФС poST во входной язык Isar системы Isabelle/HOL и на ее основе реализован генератор теории Isabelle/HOL для poST-программ.

Генерация теории Isabelle/HOL производится по описанию шаблонов требований на специализированном языке DV-RPL (requirement pattern language). Теория Isabelle/HOL состоит из: 1) набора предопределенных типов и функций; 2) вспомогательных лемм и скриптов доказательства этих лемм, получаемые из описанных в DV-RPL-спецификации шаблонов; 3) условий корректности, как теорем в этой теории, и информации об используемых для их доказательства скриптов.

Генератор теорий Isabelle/HOL для poST-программ был успешно применен при автоматическом доказательстве корректности на корпусе из 16-ти типовых poST-программ.

Публикации

1. I. Chernenko and I. Anureev, "Generation of Isabelle/HOL Theory Focused on Proving Verification Conditions of PoST Programs and Based on Derived Requirement Patterns," 2025 IEEE 26th International Conference of Young Professionals in Electron Devices and Materials (EDM), Altai, Russian Federation, 2025, pp. 1480-1485, doi: 10.1109/EDM65517.2025.11096665.

Программно-алгоритмические средства формальной верификации процесс-ориентированных программ на платформе Rodin

Разработано описание операционной семантики конструкций предложенного ранее при участии авторов процесс-ориентированного языка Reflex (предназначенного для создания управляющих программ систем промышленной автоматизации) в терминах языка Event-B (входного языка открытой платформы формальной верификации Rodin, реализованной в пакете разработки модульных кроссплатформенных приложений Eclipse).

Существующая интегрированная среда разработки (IDE) языка Reflex расширена кодогенератором, реализующим предложенные правила трансляции Reflex-программ в Event-B проекцию. Проведена практическая апробация предложенного решения на модельных управляющих программах из области промышленной автоматизации.

Решением Ученого совета полученный результат принят в качестве важнейшего результата Института автоматики и электрометрии СО РАН за 2025 год.

Разработка языка формального описания требований, ориентированного на дедуктивную верификацию poST-программ

 Рис. Фрагмент спецификации на языке poST-AL

Предложен язык формального описания требований poST-AL (annotation language), включающий два подъязыка DV-TRL (temporal requirement language) и DV-RPL (requirement pattern language).

В предлагаемом подходе на языке DV-TRL задаются темпоральные свойства программы в логике первого порядка. А на языке DV-RPL задаются: (а) базовые шаблоны требований, объединяемые в библиотеку, (б) производные шаблоны, как композиция базовых шаблонов, и (в) требования, как инстанцирование производных шаблонов конкретными значениями параметров из верифицируемой программы.

Модуль интерпретации языка TRL реализован средствами Isabelle/HOL. Модуль трансляции RPL-спецификации в теорию Isabelle/HOL реализован в фреймворке Eclipse/Xtext.

Публикации

1. I. Chernenko and I. Anureev, "Generation of Isabelle/HOL Theory Focused on Proving Verification Conditions of PoST Programs and Based on Derived Requirement Patterns," 2025 IEEE 26th International Conference of Young Professionals in Electron Devices and Materials (EDM), Altai, Russian Federation, 2025, pp. 1480-1485, doi: 10.1109/EDM65517.2025.11096665.

Метод разработки контролируемого естественного языка для шаблонов формальных спецификаций с помощью ИИ-ассистента

 Рис. Этапы разработки контролируемого естественного языка

Был разработан метод систематического построения с помощью ИИ-ассистента контролируемого естественного языка для задания требований, основанных на шаблонах формальных спецификаций, которые содержат логические атрибуты. Метод включает три этапа: 1) составление генерализованного шаблона требования на естественном языке, задействующего все атрибуты шаблона формальной спецификации; 2) генерация с помощью ИИ-ассистента корпуса шаблонов требований на естественном языке, редуцированных за счет частичного означивания атрибутов (в разработанном промпте используется генерализованный шаблон, означивание атрибутов и конкретная формальная семантика шаблонов требований); 3) формализация синтаксиса целевого контролируемого естественного языка на основе анализа грамматической структуры полученных шаблонов. Метод апробирован для EDTL-требований к КФС. Отмечено, что анализ грамматической структуры шаблонов упрощается за счет используемого LLM-метода генерации.

Язык poST – процесс-ориентированное расширение языка IEC 61131-3 Structured Text

 Рис. 1. Фрагмент кода на языке poST (демоверсия транслятора poST-программ в язык IEC 61131-3 Structured Text, https://post2st.iae.nsk.su)

Предложен язык poST — процессно-ориентированного расширения языка Structured Text (ST) стандарта IEC 61131-3. Назначение языка – программирование алгоритмически сложных управляющих программ для программируемых логических контроллеров (ПЛК) в контексте стандарта IEC 61131-3 и обеспечение согласованности исходного кода с технологическим описанием автоматизируемого процесса. poST-программа представляет собой совокупность слабо связанных параллельных процессов. Язык сочетает в себе преимущества программирования на основе машины конечных состояний с обычным синтаксисом языка ST, что облегчает его адаптацию ПЛК-сообществом. Определен базовый синтаксис языка poST и продемонстрирована эффективность его использования на модельной задаче управления лифтом за счет встроенного контроля семантики, повышения модифицируемости программ, исключения рутинных операций и сокращения общего объема исходного кода.

Публикации

1. V. E. Zyubin, A. S. Rozov, I. S. Anureev, N. O. Garanina and V. Vyatkin, "poST: A Process-Oriented Extension of the IEC 61131-3 Structured Text Language," in IEEE Access, vol. 10, pp. 35238-35250, 2022, https://doi.org/10.1109/ACCESS.2022.3157601.

Топологически свободный способ программирования киберфизических систем на основе процесс-ориентированной парадигмы

 Рис. 1. Экспериментальный стенд прототипирования распределенной системы управления системой розлива бутылок на базе CAN bus и микроконтроллеров ATmega.

Предложена концепция топологически независимой спецификации алгоритмов распределенного управления на основе парадигмы процессно-ориентированного программирования. Концепция предполагает централизованное описание алгоритма в виде множества процессов, дальнейшее разбиение процессов на множество независимых или слабозависимых кластеров и последующее развертывание полученных кластеров (или групп кластеров) на отдельных микроконтроллерных узлах распределенной системы управления. Предложен алгоритм выделения кластеров на основе анализа возможного недетерминизма при доступе к входным/выходным сигналам и межпроцессном взаимодействии, в том числе, в силу циклической зависимости процессов по управлению. Эмпирические исследования подхода на модельных задачах управления линией розлива бутылок и шлюзам показали, что процесс-ориентированная спецификация позволяет формировать мелкозернистые структуры с кластерами, которые содержат в среднем 2 процесса.

Публикации

1. Zyubin, V.E.; Garanina, N.O.; Anureev, I.S.; Staroletov, S.M. Towards Topology-Free Programming for Cyber-Physical Systems with Process-Oriented Paradigm. Sensors 2023, 23, 6216. https://doi.org/10.3390/s23136216.

2. V. E. Zyubin, D. S. Ivanishkin and I. S. Anureev, "Towards Process-Oriented Programming Distributed Control Systems," 2023 IEEE 24th International Conference of Young Professionals in Electron Devices and Materials (EDM), Novosibirsk, Russian Federation, 2023, pp. 1840-1843, https://doi.org/10.1109/EDM58354.2023.10225024. 

Процесс-ориентированный язык IndustrialC для программирования микроконтроллеров во встраиваемых системах

Рис.1. Вычислительный метод для определения реакции микроконтроллерной встраиваемой системы на внешнее событие на основе фонового гиперпроцесса (bkgHP) и гиперпроцессов прерываний (intHPi). Гиперпроцессы прерываний, которые технически представляют собой процедуры обработки прерываний, активируются по аппаратным прерываниям (inti). После завершения цикла активации управление возвращается фоновому гиперпроцессу через механизм ReTurn from Interrupt (rti).

В рамках процесс-ориентированной методологии создания ПО реактивных систем:

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

2. Предложен вычислительный метод для определения реакции микроконтроллерной встраиваемой системы на внешнее событие, реализующий разработанную модель (Рис. 1). Метод предполагает в качестве источников активации использовать прерывания как от внешних сигналов, так и от периферийных устройств микроконтроллера.

3. Для спецификации конкретного алгоритма разработан язык программирования IndustrialC, расширяющий языки Си и Reflex конструкциями для работы с аппаратными прерываниями.

Комплекс программ, реализующий предложенные модель и метод и ориентированный на микроконтроллерные платформы серии AVR, реализован в виде интегрированной среды разработки на базе пакетов Notepad++, Flex/Bison, GCC. Полученные средства прошли успешную технологическую апробацию на проектах по созданию гаммы микроконтроллерных встраиваемых систем: веб-метеосервер, автоматизированная установка термовакуумного напыления, станция термотренировки образцов SorbiPrep.

Публикации

1. Розов А. С., Зюбин В. Е. Адаптация процесс-ориентированного подхода к разработке встраиваемых микроконтроллерных систем // Автометрия. 2019. Том 55, № 2, С. 114–122 (DOI: 10.15372/AUT20190212)

2. Rozov A., Anureev I., Garanina, N., Liakh T., Zyubin V. Towards Safe Embedded Systems:IndustrialC Translational Semantics for AVR Microcontrollers. // SibirCon 2019, Novosibirsk, 21-22 October 2019.

Архитектура системы динамической верификации Reflex-программ

Рис. 1. Схема автоматической верификации алгоритмов управления: 1 – очередь выходных сообщений от АУ, 2 – блок верификации (БВ), 3 – очередь сообщений для БВ от блока управления сценариями (БУС), 4 – алгоритм управления (АУ), 5 – буфер входных сигналов АУ, 6 – буфер выходных сигналов АУ. Используется для имитации выходных аналоговых сигналов (ЦАП), 7 – виртуальный объект управления (ВОУ), 8 – очередь сообщений для передачи штатных команд от БУС к АУ, 9 – блок управления сценариями (БУС), 10 – очередь сообщений от БУС к ВОУ, 11 – очередь сообщений от БВ к БУС.

Разработана четырехкомпонентная архитектура системы динамической верификации Reflex-программ на симуляторах [1-3] (рис. 1). В отличие от автоматизированной верификации управление сценариями работы производится алгоритмическим блоком управления сценариями (БУС) (9), а контроль реакции алгоритма – алгоритмическим блоком верификации (БВ) (2). БУС через штатную очередь сообщений (8) посылает команды для АУ (4), имитируя действия оператора, а также управляет поведением ВОУ (7) через очередь сообщений (10). При этом ВОУ эмулирует как штатную работу объекта управления, так отказы его элементов. Параллельно БУС передает информацию о запускаемых сценариях в БВ через очередь сообщений (3). В свою очередь БВ на основании информации о запускаемых сценариях, сообщений от АУ, передаваемых через буфер сообщений (1) и состояния буферов входных/выходных сигналов АУ (5, 6) определяет корректность АУ.

Публикации

1. Лях Т. В., Зюбин В. Е., Гаранина Н. О. Автоматическая верификация алгоритмов управления в киберфизических системах на программных имитаторах // Автометрия. 2019. Том 55, № 2, С. 103–113 (DOI: 10.15372/AUT20190211)

2. Liakh T., Rozov A., Zyubin V. LabVIEW-based Automatic Verification of Process-Oriented Software // IEEE International Siberian Conference on Control and Communications (SIBCON-2019), April 18–20, 2019 Tomsk, Russia DOI 10.1109/SIBCON.2019.8729596

3. Liakh T., Anureev I., Garanina, Rozov A., Zyubin V. Four-Component Model for Dynamic Verification of Process-Oriented Control Software for Cyber-Physical Systems. // SibirCon 2019, Novosibirsk, 21-22 October 2019 (Scopus).

Формальная семантика языка Reflex, ориентированная на дедуктивную верификацию

Определены формальная операционная семантика языка Reflex и трансформационная семантика языка Reflex в язык Си [1-4], ориентированные на дедуктивную верификацию. Показано, что трансформационная семантика отображает программы на языке Reflex к подмножеству языка Си с формальной операционной и аксиоматической семантиками, для которого имеются методы дедуктивной верификации с использованием решателей условий корректности Z3 и ACL2.

Публикации

1. Anureev I., Garanina N., Liakh T., Rozov A., Zyubin V. Towards safe cyber-physical systems: the Reflex language and its transformational semantics // IEEE International Siberian Conference on Control and Communications (SIBCON-2019), April 18–20, 2019 Tomsk, Russia 10.1109/SIBCON.2019.8729633
2. Anureev I.S., Garanina N.O., Liakh T.V., Rozov A.S., Zyubin V.E., Gorlatch S. Two-Step Deductive Verification of Control Software Using Reflex // Proceedings of A. P. Ershov Informatics Conference (PSI-19). A. P. Ershov Institute of Informatics Systems: IPC NSU, Novosibirsk, Russia. LNCS. 2019. Vol. 11964. P. 50-63. DOI 10.1007/978-3-030-37487-7_5.
3. Anureev I. Operational Semantics of Reflex // System Informatics. 2019. No 14. P. 1-10.
4. Ануреев И.С. Операционная семантика аннотированных Reflex программ // Моделирование и анализ информационных систем. 2019. Т. 26. № 4. С. 475-487.

Исследование применимости методов онтологического проектирования
для задач формальной спецификации реактивных систем

Рассмотрены примеры формализации реактивных систем (на примере систем управления) методами, основанными на онтологии процессов, семантически-размеченной онтологии процессов и процесс-ориентированной онтологии шаблонов семантической разметки [1-4]. Показано, что онтология процессов специфицирует компактную универсальную модель процессов с возможностью определения формальной семантики как помеченной системы переходов. Эта семантика обеспечивает возможность применения формальных методов верификации, в частности, дедуктивную верификацию и проверку моделей. Вторая онтология обеспечивает возможность связывания абстрактных процессов и их элементов с понятиями предметной области (семантическую разметку) и описания новых предметно-ориентированных онтологических классов. Третья онтология задает ограничения на семантическую разметку экземпляров второй онтологии, конкретизируя понятия предметной области, связанные с этими экземплярами. Все три онтологии базируются на простых концепциях, которые могут быть использованы как онтологические шаблоны проектирования.

Публикации

1. Natalia Garanina, Igor Anureev and Vladimir Zyubin Constructing Verification-Oriented Domain-Specific Process Ontologies // System Informatics. 2019. No 14. P. 19-30.

2. Гаранина Н.О., Ануреев И.С., Зюбин В.Е. Методы специализации онтологии процессов, ориентированной на верификацию // Моделирование и анализ информационных систем. 2019. Т. 26, №4 (2019), С. 534-549.

3. Natalia Garanina, Igor Anureev, Elena Sidorova, Vladimir Zyubin and Sergei Gorlatch, An ontology-based approach to support formal verification of concurrent systems // 8th International Symposium “From Data to Models and Back (DataMod)” Porto, Portugal, 7-8 October 2019 http://pages.di.unipi.it/datamod/edition-2019/  (Scopus)

4. Staroletov S., Shilov N., Zyubin V., Liakh T., Rozov A., Konyukhov I., Shilov I., Baar T., Schulte H. “Model-driven methods to design of reliable multiagent cyber-physical systems”. In: CEUR Workshop Proceedings Vol. 2478, 2019, P. 74-91 / Modeling and Analysis of Complex Systems and Processes Workshop, MACSPro 2019; Vienna; Austria; 21-23 March 2019. P. 1-18. (Scopus)

Исследование нейросетевых решений для задачи выделения краев

Проведено исследование фильтров для нейронов первого слоя, ориентированных на задачу выделения краев. Обучение нейросети с помощью алгоритма на базе косинусной меры показало существенно более худшие результаты по сравнению с алгоритмом обратного распространения ошибки. Определены оптимальные параметры функционирования нейронов первого слоя. Предложена архитектура нейронной сети, ориентированная на задачу выделения выделения краёв [1].

Публикации

1. Кугаевских А.В., Согрешилин А.А. Анализ эффективности выделения границ сегментов средствами нейронных сетей. Автометрия, 55 (4), 2019, 118-128. DOI: 10.15372/AUT20190413

Формальная модель программы ПЛК как система переходов гиперпроцессов и темпоральная логика cycle-LTL

Предложена формальная модель программы ПЛК в виде системы переходов гиперпроцессов и темпоральная логика cycle-LTL на основе логики LTL. В предлагаемой cycle-LTL логике цикл управления рассматривается двояким образом: как воздействие окружения (в частности, объекта управления) на систему управления и как воздействие системы управления на окружение. Для каждого из этих случаев вводятся модификации стандартных темпоральных операторов логики LTL. В дополнение к этому определяются модификации (относительно базовой LTL) темпоральных операторов, действующие внутри цикла управления. Описана трансляция формул логики cycle-LTL в формулы логики LTL и доказана корректность преобразования. Сделан вывод о возможности сведения задачи верификации методом проверки моделей для требований, заданных в логике cycle-LTL, к задаче верификации требований, определённых в логике LTL.

Публикации

1. Tatiana V. Liakh, Natalia O. Garanina, Igor S. Anureev, Vladimir E. Zyubin Verifying Reflex-software with SPIN: Hand Dryer Case Study // XXI International Conference of Young Specialists on Micro/Nanotechnologies and Electron Devices, Novosibirsk, 29 June - 3 July 2020, P. 210-214

2. T. Liakh and A. Grivtsova, "Dynamic Verification of Process-Oriented Control Software by the Case of Crossroad Control," 2020 International Russian Automation Conference (RusAutoCon), Sochi, Russia, 2020, pp. 1037-1041, doi: 10.1109/RusAutoCon49822.2020.9208138.

3. Garanina N., Anureev I., Sidorova E., Koznov D., Zyubin V., Gorlatch S. (2020) An Ontology-Based Approach to Support Formal Verification of Concurrent Systems. In: Sekerinski E. et al. (eds) Formal Methods. FM 2019 International Workshops. FM 2019. Lecture Notes in Computer Science, vol 12232. Springer, Cham. https://doi.org/10.1007/978-3-030-54994-7_9

4. Garanina N., Anureev I., Zyubin V., Rozov A., Liakh T., Gorlatch S. Reasoning about Programmable Logic Controllers // System Informatics. N 17. 2020. P. 33-42.

5. Garanina N.O., Anureev I.S, Zyubin V.E. Constructing verification-oriented domain-specific process ontologies // Aut. Control Comp. Sci. 54, Issue 7, pp. 739–749 (2020) DOI: 10.3103/S014641162007007X

6. Гаранина Н.О., Ануреев И.С., Зюбин В.Е., Старолетов С.М., Розов А.С., Лях Т.В., Горлач С.П. Темпоральная логика для программируемых логических контроллеров // Моделирование и анализ информационных систем. Т. 27. № 4. 2020. С. 376-391. DOI: 10.18255/1818-1015-2020-4-376-391

Метод дедуктивной верификации управляющих программ на процесс-ориентированном языке Reflex

Рис. 1. Схема дедуктивной верификации Reflex-программ

Предложен метод дедуктивной верификации аннотированных Reflex-программ (Рис. 1), который включает четыре шага: 1) аннотирование исходной Reflex-программы через задание условий запуска, ограничений на окружение и инвариантов цикла управления, 2) трансляцию аннотированной Reflex-программы в аннотированную Си программу, 3) генерацию условий корректности для результирующей Си программы, 4) доказательство порожденных условий корректности. В качестве формального обоснования метода разработаны: 1) операционная семантика аннотированных Reflex программ, 2) трансформационная семантика Reflex-программ в язык Си, 3) аксиоматическая семантика полученных в результате трансляции аннотированных Си программ. Метод апробирован на тестовой управляющей программе с использованием SMT-решателя Z3. Предложенный метод является первым методом формальной верификации процесс-ориентированных программ и направлен на контроль качества программного обеспечения для программируемых логических контроллеров.

Публикации

1. Anureev I., Garanina N., Liakh T., Rozov A., Zyubin V. Towards safe cyber-physical systems: the Reflex language and its transformational semantics // IEEE International Siberian Conference on Control and Communications (SIBCON-2019), April 18–20, 2019 Tomsk, Russia. DOI 10.1109/SIBCON.2019.8729633

2. Anureev I., Garanina N., Liakh T., Rozov A., Zyubin V., Gorlatch S. (2019) Two-Step Deductive Verification of Control Software Using Reflex // Lecture Notes in Computer Science, Vol 11964. 2019. P. 50-63. DOI 0.1007/978-3-030-37487-7_5

3. Anureev I.S. Operational semantics of Reflex // System Informatics. N 14. 2019. P. 1-10. DOI 10.31144/si.2307-6410.2019.n14.p1-10

4. Ануреев И.С. Операционная семантика аннотированных Reflex программ // Моделирование и анализ информационных систем. Т. 26. № 4. 2019. С. 475-487

5. Ануреев И.С., Гаранина Н.О., Лях Т.В., Розов А.С., Зюбин В.Е., Горлач С.П. Дедуктивная верификация Reflex-программ // Программирование. 2020. № 4. С. 14-26.

Исследование применимости модели end-stopped нейрона для задач точного определения границ при сегментации изображения

Рис. Схема работы нейрона по модели CE 

Проведено исследование модели нейрона конца линий для задач определения границ при сегментации изображения и предложена CE-модель комплексного нейрона конца линий, обеспечивающего высокий отклик на конце линии. Предложенная CE-модель нейрона конца линий базируется на фильтрах Габора, находящихся в противофазе. Предложенная модель интегрирована в сверточную нейронную сеть выделения краев. В результате исследования было установлено, что габоровская B-V модель не позволяет с точностью до пикселя выделять конец линии. Реакция нейрона конца линий в неокогнитроне отличается во втором знаке после запятой, что может нивелироваться колебаниями яркости пикселей на естественном изображении. Модель Хейтгера и предложенная модель CE близки и показывают высокую селективную способность, но модель Хейтгера более сложна в вычислительном плане. К тому же, вычисление квадратурной пары фильтров Габора, необходимое для энергии Габора, оправданно для цифровой обработки сигналов, где выравнивает влияние низких частот. При работе с изображением в пространстве CIE L*a*b* в этом нет необходимости. Еще одним достоинством предлагаемой модели является легкая интеграция со сверточными нейронными сетями, где функция рецепторов базируется на использовании фильтра Габора.

Публикации

1. A. Kugaevskikh, "Bio-Inspired End-Stopped Neuron Model for the Curves Segmentation," 2020 International Russian Automation Conference (RusAutoCon), Sochi, Russia, 2020, pp. 719-724, doi: 10.1109/RusAutoCon49822.2020.9208069.

2. Kugaevskikh A.V., Grif M.G. Recognition of deaf gestures based on a bio-inspired neural network. Journal of Physics: Conference Series. 2020. Vol. 1661. P. 012038. DOI: 10.1088/1742-6596/1661/1/012038

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

 Рис. 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