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

Індекс рубрикатора НБУВ: В126я73-1

Шифр НБУВ: ВА624356 Пошук видання у каталогах НБУВ 

Описано програмні засоби, що реалізують профілювання різних аспектів виконання АПЛАН-програм, які використовуються в системі алгебричного програмування. Розглянуто застосування засобів профілювання для оцінки якості програм за допомогою вимірювання покриття та дослідження програм на "вузькі місця" щодо швидкості та пам'яті.

Розглянуто методи роботи з вимогами, що складають технологію, яка є складовою частиною процесу створення програмних систем з великою кількістю станів. Висвітлено п'ять складових частин цієї технології: формалізацію вимог у вигляді базових протоколів, пошук суперечливостей та неповноти, генерацію тестових наборів з множини вимог, синтез та аналіз динамічних властивостей моделі. Вимоги до інтерактивних систем представлено у вигляді формальних специфікацій - базових протоколів. Визначено клас базових протоколів, для якого задачі технології вирішуються без експонентного вибуху. За допомогою формалізму побудовано алгоритми верифікації базових протоколів з використанням машини доведення, а також синтез моделі за базовими протоколами. На основі методів символьного моделювання розглянуто різні критерії генерації тестів та їх застосування до генерації тестів за специфікаціями, записаними сучасними інженерними мовами - MSC, SDL, UML.

Розглянуто загальні підходи В. М. Глушкова до проблеми штучного інтелекту. Зокрема, детально висвітлено історію досліджень за програмою "Алгоритм Очевидності", ініційованою В. М. Глушковим. Проаналізовано результати, одержані за цією програмою.

Розглянуто творчий науковий шлях видатного вченого XX ст., піонера в галузі інформатики й кібернетики академіка Віктора Михайловича Глушкова, відомого своїми науковими досягненнями світового значення в галузі математики, інформатики, кібернетики, обчислювальної техніки і програмування, створення ним потужних наукових шкіл за цими напрямами. Основну увагу приділено математичним роботам і архітектурним ідеям В. М. Глушкова, пов'язаним з інтелектуалізацією комп'ютерів та втіленням однієї з найяскравіших його мрій - створенням комп'ютерної моделі людського розуму.

Висвітлено питання рішення задачі розробки високонадійних систем, зокрема тих, що критичні до безпеки. Розглянуто проблеми тестування та верифікації, які актуальні на кожній стадії процесу розробки. Окрім того під час розробки мають бути дотримані такі стандарти розробки систем як досяжність 100 % тестового покриття та застосування технології модельного тестування для розподільних і недетермінованих систем. Запропоновано розв'язання проблеми з використання символьних методів на основі теорії інсерційного моделювання та предикатних перетворювачів. Як формальні специфікації, що визначають модель системи використовується мова Live UCM, як композиція стандартної мови UCM (Use Case Maps) та мова базових протоколів. Запропоновані методи реалізовані в низці програмних систем та апробовані на прикладах перевірки властивостей безпеки в моделях у проектах в різних галузях сучасної індустрії.

Вирішено важливу індустріальну проблему розробки високонадійних систем, зокрема, систем, що критичні до безпеки. Розглянуто проблеми тестування, верифікації та реверсної інженерії, які актуальні на кожній стадії процесу розробки. Надано огляд сучасного стану систем і методів модельного тестування та верифікації. Визначено специфікації моделей систем критичних до безпеки у вигляді нотації Live UCM. Розширено клас предикатних перетворювачів для вирішення завдань символьного моделювання. Розглянуто семантику методу трасової генерації для Live UCM специфікацій. Розроблено методику модельного тестування на основі методів "чорної скриньки" та "білої скриньки", методи верифікації із застосування інваріантів, а також розглянуто методи перетворення моделей для цілей реверсної інженерії.

Доповідь присвячено важливій проблемі створення методів та алгоритмів побудови високонадійних систем математичного забезпечення для програмно-технічних комплексів, які використовуються в критичних з точки зору безпеки галузях, таких як аерокосмічна, медична, телекомунікаційна, в ядерній енергетиці, у виробництві сучасного озброєння тощо. Процес розроблення високонадійних систем оснований на принципі зменшення ризику або повного виключення неспрацьовування засобів безпеки в системі.

Науковий доробок В. К. Дзядика складають понад 160 публікацій, серед них 4 монографії, він також є автором новаторського підручника з математичного аналізу. Наукову працю талановитий учений поєднував із педагогічною діяльністю, спрямованою на відшукання обдарованої талановитої молоді і залучення її до активної математичної роботи. Впродовж багатьох десятиліть він читав основні і спеціальні курси з математичного аналізу для студентів Київського державного університету ім. Тараса Шевченка та Луцького педагогічного інституту ім. Лесі Українки. Математична обдарованість, педагогічна майстерність, уважне і чуйне ставлення до молодих дослідників надали змогу В. К. Дзядику заснувати нині визнану в усьому світі наукову школу з теорії наближення функцій, яка об'єднує спеціалістів з теорії наближення, математичного аналізу та обчислювальної математики, котрі успішно працюють у різних наукових та освітніх центрах в Україні та за її межами.

Пошук вразливостей у програмному забезпеченні є на поточний момент актуальним завданням і джерелом наукових викликів. Описаний у алгебричний підхід покликаний збільшити ефективність і достовірність алгоритмів пошуку. Запропоновано засоби формального опису поведінки бінарного коду та вразливостей у термінах алгебри поведінок, а також двоступеневий загальний алгоритм пошуку, описано прототип відповідної програмної системи.

Проаналізовано напрямки застосування та використання децентралізованих (розподілених) систем на прикладі технології блокчейн в міжнародній логістиці. Розглянуто перспективи та ключові аспекти подальшого розвитку децентралізованих систем та великих баз даних. Розглянуто основи функціонування смарт-контрактів на базі Etherium та мови Solidity. Проаналізовано основні проблеми безпеки в цілісному ланцюгу постачання, виявлено напрямки покращення відслідковування безперервності контролю якості товару під час руху в мультимодальному ланцюгу постачання. Запропоновано методи посилення контролю за безпекою в децентралізованих системах у логістиці. Розглянуто методологію формальних алгебраїчних методів з метою аналізу та дослідження властивостей перевезень при взаємодії агентів певного логістичного середовища.

Розглянуто технологію нечіткого тестування, яка полягає у тестуванні програмних систем із поданням критичних або неочікуваних вхідних даних. Наведено огляд поточного стану проблеми та основні системи нечіткого тестування. Проаналізовано підхід до технології нечіткого тестування з використанням алгебричних методів, зокрема символьного моделювання. Розглянуто алгоритм "легкої ваги", який розроблено для скорочення часу генерації тестів. Алгоритм реалізовано в середовищі системи інсерційного моделювання та апробовано в тестуванні давно відомих версій систем, розроблених в ОС Linux.

Досліджено проблему інсерційної семантики специфікацій апаратного забезпечення, зокрема мови VHDL. Побудова семантики потрібна для представлення первинного коду мови VHDL у вигляді інсерційної моделі за допомогою алгебри поведінок. Це представлення надає змогу широко застосовувати формальні методи інсерційного моделювання для верифікації електронних проектів критичних систем. Розглянуто основні конструкції мови VHDL, зокрема процес, архітектуру, паралельні оператори, та їхню інсерційну семантику. У вигляді поведінкових рівнянь побудовано потік керування VHDL-програми. Послідовні оператори представлено як дії алгебри поведінок. Розглянуто проблему перегонів сигналів і методів її виявлення через визначення властивості переставності (permutability).

Розглянуто основні методи молекулярного моделювання та спеціалізоване програмне забезпечення для створення та дослідження молекулярних моделей. Наведено результати першого етапу побудови середовища для дослідження молекулярної і біомолекулярної взаємодії, що базується на формалізмі алгебри поведінки та інсерційного моделювання, а також результати експерименту застосування запропонованого підходу до моделювання ковалентного неполярного зв'язку.

Міжнародна та внутрішня обслуговуюча логістика розвивається шаленими темпами у сучасному житті, а прогнози на майбутнє для цієї галузі оптимістичні. З цих причин ми постали перед задачею контролю, оптимізації, безпечної та надійної перевірки комплексних логістичних систем з багатьма внутрішніми агентами, які працюють у середовищі, що змінюється. Дана робота має на меті показати як математичне моделювання, зокрема, алгебра поведінок, надає можливість передбачувати поведінку, стабільність логістичних середовищ та перевіряти їх властивості безпеки, та надійності. Ці процедури є модельно-орієнтованими розробками комплексних систем програмного забезпечення, таких як логістичні системи.

Із різким зростанням темпу розвитку технологій і впровадженням їх в інфраструктуру підприємств різних сфер діяльності виникає потреба в аналогічному розвитку засобів мережевої безпеки. Сучасні мережі мають багато точок доступу та обробляють великі обсяги трафіку. У зв'язку з залежністю від підключення до інтернет і використання хмарних сервісів, зростає інтерес до приватної інформації в мережі, з'являється все більше підходів до атак, кіберзлочинність стає більш винахідливою у використанні нових технологій. Таким чином, система захисту повинна мати можливість виявляти нові типи вторгнень з високою точністю та мінімальним числом хибних спрацювань. Ключову роль у засобах безпеки грає виявлення вторгнень і можливість заблокувати вторгнення порушника в реальному часі. Активний підхід до кібербезпеки, що надає змогу виявляти потенційні загрози та швидко реагувати, надають системи виявлення вторгнень, що можуть перевіряти мережевий трафік, виявляти шкідливі програми та запобігати будь-якій підозрілій активності. Мета роботи - показати основні види систем виявлення вторгнень та описати їх принцип роботи. Зокрема, з метою знайти систему, що відповідатиме новим поставленим вимогам, розглянуто 2 ефективних підходи: метод алгебричного зіставлення на основі алгебричного моделювання та метод виявлення вторгнень із використанням нейронних мереж. Для перевірки та порівняння ефективності обох методів створено прототипи систем, націлених на виявлення однієї з найпоширеніших атак типу "людина - посередник" - ARP Spoofing. За результатами аналізу їх переваг і недоліків запропоновано новий підхід, а саме, комбінацію обох підходів, що включає їх сильні сторони та має перспективи для розвитку.

Розглянуто методи виявлення кібератак у реальному часі, що базуються на алгебричному підході. Застосовано метод алгебричного зіставлення, в основу якого покладено методи розв'язання поведінкових рівнянь та алгебричного моделювання. Водночас для підвищення ефективності виявлення та запобігання запропоновано використовувати композицію нейронної мережі для класифікації атак і методу алгебричного зіставлення. Цю конструкцію називають когнітивною мережею, поняття якої вперше було сформульовано у 2005 р. Розглянуто такі властивості когнітивної мережі, як подвійна класифікація та самонавчання. Наведено технологічну лінію для виявлення кібератак із використанням когнітивних мереж.