Дослідження та застосування
Кібербезпека
Створено технологію виявлення вразливостей в бінарному коді.
Визначено семантику інструкцій для бінарного коду процесора Intel x86 у вигляді специфікацій алгебри поведінок.
Створено алгоритми алгебраїчного співставлення поведінок та символьного моделювання з використанням шаблонів вразливостей.
Створено технологію формалізації шаблонів вразливостей та атак.
Запропоновано гібрідну технологію виявлення атак в мережевому середовищі з використанням алгебраїчного підходу та машинного навчання.
Верифікація та тестування систем апаратного забезпечення.
Технологію верифікації та модельного тестування було адаптовано для апаратного забезпечення та інтегровано із мовою специфікацій VHDL.
Апробація методів верифікації та тестування проводилось в ході виконання промислових проектів НВП «Радій» м. Кропивницький. Були отримані вагомі результати отримані під час розв’язання наступних задач формальної верифікації. По-перше, виконано алгебраїчний опис обраного фрагмента специфікації вимог для електронних компонент проекту, які реалізовано мовою VHDL. Для фрагменту специфікації вимог виконано аналіз наявності порушень характеристик несуперечливості, повноти та інше, що є особливо важливим для процесів верифікації цифрових пристроїв. Одержано тестові набори для проведення функціональної (поведінкової) симуляції роботи обраного бібліотечного ком1понента. Цей результат дозволяє знизити суб’єктивні ризики виконання поведінкового тестування, тобто знизити ризики якості формулювання вимог розробником та їх розуміння тестувальником, а також якості та кількості тестових наборів, які розроблюються та виконуються з цифровим пристроєм. По-друге, виконано алгебраїчний опис набору сценаріїв логік користувача User Application Logic (UAL), які виконуються програмованим логічним контролером (ПЛК), у процесі чого визначено ймовірні критичні шляхи виконання цих логік.
Верифікація та формалізація кібер-фізичних систем
Розширено алгебру поведінок для формалізації та моделювання систем в яких присутня неперервна компонента. Досліджено деякі моделі та проведено експерименти з верифікації кібер-фізичних систем на прикладі апаратного забезпечення. Дані експерименту стали основою архітектури системи аналізу поведінок компонент апаратного забезпечення з метою виявлення температурних та електромагнітних аномалій, хибного спрацювання у вентильних матрицях та мікроконтролерах.
Координація наукової діяльності
Відділ виступає як провідний у розвитку досліджень з алгебричного програмування та інсерційного моделювання в Україні та у світі, співпрацює з вищими навчальними закладами країни та з установами, що займаються розробкою програмного забезпечення, поширюючи набуті знання, новітні методи та впроваджуючи результати досліджень.
У відділі постійно працює науковий семінар.
Міжнародні зв’язки
Відділ підтримує наукові зв’язки з США (фірма Google, Cadence, Amazon), Великобританією (Лондонський університетський коледж, Лідський університет Бекета, університет Глазго), Ірландією (Університетський Коледж Дублін), Болгарією(Інститут інформації та комунікаційних технологій), Австрією (Інститут символьних обчислень Лінц, Технічний університет Відень), Академією наук Молдови (Інститут математики і інформатики), Китай (компанія Huawei)
Скобелєв В.Г. є членом редколегій двох закордонних журналів:
“International Journal of Trendy Research in Engineering and Technology” (IJTRET), India.
“Computer Science Journal of Moldova” (CSJM), Republic of Moldova.
