Институт в фотографиях

2023 г.

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

2021 EDTL fig1 rus

 

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


2022 г.

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

2021 EDTL fig1 rus

 

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

 


2021 г.

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

2021 EDTL fig1 rus

 

 Рис. 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-программы

 2021 fig2 cyclicLTL  

Предложена система переходов гиперпроцессов (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

 


2020 г.

Формальная модель программы ПЛК как система переходов гиперпроцессов и темпоральная логика 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

20 fig1

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

 


2019 г.

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

19 fig2

Рис.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-программ

19 fig1

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