Процесс-ориентированный язык 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