Манжос Юрій Семенович. Семантичні моделі, методи та інформаційна технологія підвищення надійності програмного забезпечення інформаційно-управляючих систем

brief description

Манжос Юрій Семенович. Семантичні моделі, методи та інформаційна технологія підвищення надійності програмного забезпечення інформаційно-управляючих систем : дис... канд. техн. наук: 05.13.06 / Національний аерокосмічний ун-т ім. М.Є.Жуковського "Харківський авіаційний ін-т". — Х., 2006. — 197арк. : рис., табл. — Бібліогр.: арк. 149-166.

Манжос Ю.С. Семантичні моделі, методи та інформаційна технологія підвищення надійності програмного забезпечення інформаційно-управляючих систем.- Рукопис.
Дисертація на здобуття наукового ступеня кандидата технічних наук за спеціальністю 05.13.06 автоматизовані системи управління і прогресивні інформаційні технології. Національний аерокосмічний університет ім. М.Є. Жуковського Харківський авіаційний інститут”, Харків, 2006.
Дисертацію присвячено підвищенню ефективності експертизи та сертифікації програмного забезпечення інформаційно-управляючих систем критичного застосування за допомогою розробки моделей та інструментальних засобів, що забезпечують незалежну семантичну верифікацію на підставі аналізу збереження на всіх проектних рівнях програмного інваріанту—семантики програмних змінних. Розроблено метод побудови семантичних моделей програмного забезпечення, обґрунтовано їх використання для верифікації. Розроблено метод оцінки достовірності незалежної верифікації — калібрування методу, заснованого на ін’єкції програмних дефектів у семантичну модель згідно зі статистичними характеристиками програмного коду. Розроблено інструментальний засіб підтримки незалежної верифікації та експертизи програмного забезпечення інформаційно-управляючих систем.

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

Проведено аналіз та класифікацію атрибутів, метрик, методів та інструментальних засобів автоматизованої верифікації та сертифікації програмного забезпечення. Зроблено висновок, що існуючі методи та інструментальні засоби не забезпечують потрібну повноту і достовірність експертизи під час сертифікації.
Обґрунтовано використання семантичних атрибутів для оцінки атрибуту якості ПЗ надійності шляхом оцінки ймовірності залишкових дефектів під час сертифікації програмного забезпечення інформаційно-управляючих систем. Набула подальшого розвитку модель якості ПЗ ІУС IEC 9126/14598, що забезпечило обґрунтування та вибір проектних рішень з диверсифікації інформаційних технологій верифікації як суперпозицію множини атрибутів завдяки врахуванню реального ступеня різноманіття атрибутів.
Розроблено та проаналізовано комплексну семантичну модель програмного забезпечення інформаційно-управляючих систем, що містить семантичне відображення, семантичний простір, семантичну алгебру, класифікацію та моделі семантичних програмних дефектів. Доведено доцільність використання семантичних атрибутів — фізичних розмірностей для формальної верифікації програмного забезпечення інформаційно-управляючих систем.
Розроблено метод незалежної верифікації, заснований на семантичній моделі програмного забезпечення, що підвищує об'єктивність оцінки якості та надійності ІУС під час незалежної експертизи та сертифікації. Вдосконалено метод статичного аналізу, що дозволило виявляти семантичні дефекти без виконання програм завдяки диверсифікації верифікації, яка досягається інструментуванням коду, для забезпечення лінеаризації та перевизначення типів даних на спеціально розроблені класи, що реалізують контроль семантичної коректності на всіх рівнях проекту. Набув подальшого розвитку адаптивний метод калібрування чутливості та ступеню різноманіття, що дозволило оцінити достовірність верифікації шляхом ін'єкції дефектів у семантичну модель та унеможливленням інтерференції і породження вторинних дефектів, через суміщення ін'єкції та виявлення дефектів з вимірюванням атрибутів програмних інваріантів. Вдосконалено метод оцінки результату верифікації, що дозволило оцінити зменшення залишкових дефектів завдяки використанню статистичних характеристики програмного коду для оцінки зниження ймовірності їх існування.

У результаті проведених досліджень та запропонованих методів розроблені методики, процедури, алгоритми та програмно реалізовано підсистему незалежної верифікації інтегрованої системи підтримки експертизи та незалежної верифікації ПЗ ІУС АЕС. В основі підсистеми — використання статичного аналізу програмного забезпечення та семантичних моделей, методів вимірювання, оцінювання атрибутів і характеристик ПЗ, забезпечило підвищення достовірності результатів експертизи та незалежної верифікації під час сертифікаційних випробувань.
У результаті дослідної експлуатації було експериментально оцінено розроблено методи підвищення надійності програмного забезпечення. Доведено ефективність моделей та методів під час сертифікаційних випробувань. Досягнуто зменшення ймовірності існування залишкових семантичних програмних дефектів у сім разів.
Подальші дослідження доцільно проводити у напрямку розвитку автоматизації всіх процесів сертифікації ПЗ, шляхом формалізації всіх процедур та їх інтеграції в єдиному середовищі, а також комплексного використання кількох інваріантів ПЗ; втілення аналізу програмного коду для різноманітних алгоритмічних мов та адаптації середовища для використання у різних галузях, наприклад аерокосмічній техніці, зв’язку, банківських системах, транспорті тощо.