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