Реєстраційний номер
0823U102005, Дисертація доктора філософії
На здобуття
Доктор філософії
Дата захисту
24-01-2024
Статус
Наказ про видачу диплома
Назва роботи
Інформаційна технологія верифікації паралельних часопараметризованих програм інформаційних управляючих систем
Здобувач
Мороз Ольга Юріївна,
Керівник Толстолузька Олена Геннадіївна
Опонент Одарущенко Олег Миколайович
Опонент Дорошенко Анатолій Юхимович
Рецензент Гамзаєв Рустам Олександрович
Рецензент Мірошник Марина Анатоліївна
Установа, організація, у вченій раді якої відбудеться/відбувся захист
Харківський національний університет імені В. Н. Каразіна
Опис
Дисертація на здобуття ступеня доктора філософії за спеціальністю 122 – Комп’ютерні науки (Галузь знань 12 – Технічні науки). – Харківський національний університет імені В. Н. Каразіна, Міністерства освіти і науки України, Харків, 2023.
Дисертація присвячена верифікації паралельних програм для інформаційних управляючих систем, що є складною та важливою задачею з багатьма проблемами та викликами.
Розглядаються особливості процесу верифікації паралельних програм інформаційних управляючих систем. Описані найпоширеніші інструментальні засоби верифікації програм з підтримкою паралельних обчислень. Приділено увагу, що на сьогодні необхідність високої ефективності паралельного програмного забезпечення інформаційних управляючих систем вимагає суттєвого розширення складу факторів, що враховуються при формальній розробці часопараметризованих мультипаралельних програм інформаційних управляючих систем. Акцентовано, що верифікація мультипаралельних часопараметризованих програм має три складові: компіляційна верифікація; декомпіляційна верифікація та семантична верифікація. Компіляційна верифікація забезпечує перевірку синтаксичної та часової коректності формального синтезу структур семантико-числової специфікації, декомпіляційна верифікація забезпечує перевірку логічної еквівалентності синтезованих мультипаралельних програм та текстів вхідних послідовних програм після завершення всіх етапів синтезу, а семантична верифікація полягає у перевірці збігу одиниць вимірювання фізичних величин, отриманих на основі формального синтезу часопараметризованих мультипаралельних програм інформаційних управляючих систем та одиниць вимірювання вхідних та вихідних даних, що задаються користувачами. Сформовано сучасні вимоги до суттєвого розширення складу факторів, що враховуються при формальній розробці часопараметризованих мультипаралельних програм інформаційних управляючих систем. Формулюється задача дисертаційного дослідження, як розробка інформаційної технології верифікації паралельних часопараметризованих програм інформаційних управляючих систем з метою підвищення її ефективності за рахунок застосування компіляційної, декомпіляційної та семантичної верифікації на основі семантико-числових специфікацій. Для вирішення поставленої науково-прикладної задачі вирішено розробити ряд методів, а саме: метод компіляційної верифікації паралельних часопараметризованих програм для інформаційних управляючих систем; метод декомпіляційної верифікації паралельних часопараметризованих програм для інформаційних управляючих систем; метод семантичної верифікації паралельних часопараметризованих програм для інформаційних управляючих систем.
Описано етапи розробки методу компіляційної верифікації паралельних програмних засобів інформаційних управляючих систем. Описані існуючі методи паралельної обробки інформації та їх сутність, показано доцільність використання сукупності методів паралельної обробки інформації при розробці паралельного програмного забезпечення інформаційних управляючих систем.
Описано сутність декомпіляційної верифікації часопараметризованих програмних засобів інформаційних управляючих систем. Починаючи з аналізу бінарного коду послідовної програми, проводиться його декомпіляція з метою відновлення вхідного коду. Отриманий вхідний код піддається формальній верифікації за допомогою математичних методів. Відбувається доведення коректності програми, перевірка властивостей безпеки, аналіз відповідності вимогам тощо. Аналізуючи вхідний код програми, можна виявити можливі вразливі місця, дефекти або помилки, що можуть впливати на її безпеку та надійність. Також описані етапи постановки задачі декомпіляційної верифікації часопараметризованих паралельних програмних засобів інформаційних управляючих систем.
Описано метод семантичної верифікації часопараметризованих мультипаралельних програм, змістовно розглянуті основні етапи методу семантичної верифікації мультипаралельних програм та описано побудову графу, що здійснюється за допомогою засобів візуалізації паралельних апаратно-програмних об’єктів. Представлена концептуальна модель технології верифікації часопараметризованих паралельних програм інформаційних управляючих систем та змістовно описано основні компоненти архітектури технології верифікації. Обрано показники ефективності технології семантико-числової верифікації інформаційних управляючих систем спрямовані на оцінку точності та надійності результатів верифікації.
Сукупність отриманих у дисертації нових наукових результатів, позитивна оцінка їхньої достовірності, наукової та практичної значущості дають змогу вважати сформульовану наукову задачу розробки технології верифікації паралельних часопараметризованих програм інформаційних управляючих систем з метою підвищення ефективності верифікації за рахунок застосування компіляційної, декомпіляційної та семантичної верифікації на основі семантико-числових специфікацій, – розв'язаною, а поставлену мету – досягнутою.
Дата реєстрації
2023-12-26
Додано/оновлено в НРАТ
2024-01-22 / 2026-07-01
