Міністерство освіти і науки України

Національний аерокосмічний університет ім. М.Є. Жуковського“

Харківський авіаційний інститут”

МАНЖОС Юрій Семенович

УДК 004.05+004.415.5

СЕМАНТИЧНІ МОДЕЛІ, МЕТОДИ ТА ІНФОРМАЦІЙНА ТЕХНОЛОГІЯ ПІДВИЩЕННЯ НАДІЙНОСТІ ПРОГРАМНОГО ЗАБЕЗПЕЧЕННЯ
ІНФОРМАЦІЙНО-УПРАВЛЯЮЧИХ СИСТЕМ

Спеціальність 05.13.06 – автоматизовані системи управління
та прогресивні інформаційні технології

Автореферат

дисертації на здобуття наукового ступеня
кандидата технічних наук

Харків – 2007

Дисертацією є рукопис.

Робота виконана у Національному аерокосмічному університеті ім. М.Є. Жуковського “Харківський авіаційний інститут”, Міністерство освіти і науки України

Науковий керівник: | доктор технічних наук, професор

Конорев Борис Михайлович,

Національний аерокосмічний університет
ім. М.Є. Жуковського “Харківський авіаційний інститут”,

професор кафедри програмного забезпечення комп’ютерних систем

Офіційні опоненти: | доктор технічних наук, професор

Жолткевич Григорій Миколайович,

Харківський національний університет ім. В.Н. Каразіна,

завідуючий кафедрою теоретичної та прикладної інформатики;

кандидат технічних наук, старший науковий співробітник

Кучук Георгій Анатолійович,

Харківський університет повітряних сил ім. І. Кожедуба,

начальник науково-дослідного відділу.

Провідна установа: | Харківський Національний університет радіоелектроніки, кафедра системотехніки, Міністерство освіти і науки України, м. Харків.

Захист відбудеться “ 16 ” лютого 2007 р. о 12 годині на засіданні спеціалізованої вченої ради Д64.062.01 у Національному аерокосмічному університеті ім. М.Є. Жуковського “Харківський авіаційний інститут” за адресою: 61070, м. Харків, вул. Чкалова, 17, радіотехнічний корпус, ауд.232.

З дисертацією можна ознайомитись у науково-технічній бібліотеці Національного аерокосмічного університету ім. М.Є. Жуковського “Харківський авіаційний інститут” за адресою:
61070 м. Харків, вул. Чкалова, 17.

Автореферат розісланий “ 13 ” січня 2007 р.

Вчений секретар

спеціалізованої вченої ради ______________ Латкін М.О.

ЗАГАЛЬНА ХАРАКТЕРИСТИКА РОБОТИ

Актуальність теми. Ефективне функціонування сучасних технічних систем неможливе без комплексної автоматизації виробничих процесів та вдосконалення керування шляхом широкого застосування прогресивних інформаційних технологій, що потребує розробки не тільки програмного забезпечення (ПЗ) для інформаційно-управляючих систем (ІУС), але і спеціалізованих інструментальних засобів для їх створення, тому що кожні десять років обсяг програмного коду ІУС критичного застосування збільшується у 10 разів. Стратегією розвитку атомної енергетики України передбачені розробка ІУС для нових енергоблоків та модернізація існуючих. Безпека експлуатації АЕС визначається якістю управляючих систем, велика частка критичних функцій яких, реалізована програмно, тому залишкові дефекти ПЗ (ДПЗ) є факторами ризику виникнення аварійних ситуацій. Базовою нормативною вимогою безпечної експлуатації ІУС є проведення незалежної верифікації. Значний внесок у розробку методів верифікації мають вітчизняні та закордонні дослідники: Б.У. Боем, Р. Глас, Б.М. Конорев, В.В. Липаєв, М. Липов, Г. Майєрс, Е. Нельсон, Т. Тейєр, В.В. Шураков та інші. Інструментальні засоби, що реалізують ці методи, мають обмеження: трудомісткість підготовки до верифікації, неможливість повного покриття всіх обчислювальних маршрутів, значну обчислювальну складність, обумовлену великою кількістю контрольних прикладів.

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

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

Зв'язок роботи з науковими програмами, планами, темами. Дослідження, результати яких викладені у дисертації, проводилися згіндо з державними планами НДР, програмами та договорами, що виконувалися у Національному аерокосмічному університеті ім. М.Є. Жуковського у рамках держбюджетних НДР Міністерства освіти і науки України на кафедрі економіко-математичного моделювання: “Розробка науково-методичних основ та інформаційних технологій оцінки і забезпечення відмовостійкості та безпеки комп’ютеризованих систем аерокосмічних комплексів, інших комплексів критичного застосування” (№ U003502) та “Теорія створення квантових систем штучного інтелекту для прийняття технологічних рішень у виробництві аерокосмічної техніки” (ДР № U004081), а також у Сертифікаційному центрі АСУ Держцентрякості державного комітету ядерного регулювання України у рамках НДР “Інтегроване інструментальне середовище підтримки експертизи та незалежної верифікації програмного забезпечення систем критичного застосування”, (наказ № 69 від 12.07.2002). Особистий внесок автора в зазначених НДР як співвиконавця полягає в розробці атрибутів, критеріїв та методик оцінки якості, моделей та методів незалежної верифікації програмного забезпечення, заснованих на використанні семантичних інваріантів для інструментальної системи автоматизації верифікації та експертизи ПЗ, що склала основу автоматизованого рабочого місця експерта сертифікаційного центру.

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

Для досягнення поставленої мети вирішуються такі задачі:

1. Проаналізувати та класифікувати відомі атрибути, метрики, методи та інструментальні засоби автоматизованої верифікації та сертифікації програмного забезпечення.

2. Обґрунтувати використання семантичних атрибутів для верифікації та експертизи програмного забезпечення інформаційно-управляючих систем.

3. Розробити та проаналізувати семантичну модель програмного забезпечення інформаційно-управляючих систем.

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

5. Розробити підсистему незалежної верифікації програмного забезпечення та впровадити її в інтегровану систему підтримки незалежної верифікації та експертизи.

6. Експериментально оцінити розроблені методи підвищення надійності програмного забезпечення.

Об’єкт дослідження— процеси верифікації та оцінювання якості і надійності програмного забезпечення інформаційно-управляючих систем.

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

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

Наукова новизна одержаних результатів:

1) вперше одержано:—

семантичну модель програмного забезпечення, що доводить доцільність використання семантичних атрибутів — фізичних розмірностей для формальної верифікації інформаційно-управляючих систем;—

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

2) удосконалено:—

метод статичного аналізу, що дозволяє виявляти семантичні дефекти програмного забезпечення без виконання програм завдяки диверсифікації верифікації, яка досягається інструментуванням коду, для забезпечення лінеаризації та перевизначення типів даних на спеціально розроблені класи, що реалізують контроль семантичної коректності на всіх рівнях проекту;—

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

3) дістали подальшого розвитку:—

модель якості програмного забезпечення інформаційно-управляючих систем IEC 9126/14598, що забезпечило обґрунтування та вибір проектних рішень з диверсифікації інформаційних технологій верифікації як суперпозицію множини атрибутів, завдяки врахуванню реального ступеня різноманіття атрибутів;—

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

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

Результати досліджень впроваджені у:–

Сертификаційному центрі АСУ Держцентрякості Державного комітету ядерного регулювання України під час розробки “Інтегрованого інструментального середовища підтримки експертизи і незалежної верифікації програмного забезпечення систем критичного застосування” для ДКЯРУ, НКАУ, НАЕК (акт впровадження від 12.04.2005);—

навчальному процесі Національного аерокосмічного університету ім. М.Є.Жуковського “ХАІ” (акт впровадження від 30.08.2006).

Достовірність нових наукових положень та висновків дисертаційної роботи підтверджується:

— коректним використанням фундаментальних положень і результатів відомих теоретичних досліджень, наведених у літературі, при побудові семантичної моделі програмного забезпечення;

— практичним впровадженням у інструментальних засобах та системах підтримки експертизи і верифікації програмного забезпечення інформаційно-управляючих систем;

— результатами експертизи програмного забезпечення конкретних систем, що довели можливість та ефективність використання семантичних інваріантів під час сертифікації.

Особистий внесок здобувача полягає у розробці нових моделей, методів, методик та інформаційної технології, які забезпечили вирішення задач, що були поставлені у дисертації. Всі основні наукові положення, результати, висновки і рекомендації роботи досягнуті автором самостійно. Роботи [2,4,6–9] були опубліковані без співавторів. У роботах, опублікованих у співавторстві, здобувачу належать: розробка семантичної моделі ПЗ [1]; розробка методології диверсифікації технологій верифікації [3]; розробка схеми даних для зберігання вимог нормативної документації та принципів побудови механізму логічного висновку [5]; розробка семантичного методу незалежної верифікації та його алгебраїчних основ [10]; вибір базису семантичного простору [11]; організація знань та принципи побудови інтелектуального аналізатора коду [12]; розробка методології інтегрованого інструментального середовища підтримки експертизи та незалежної верифікації [13]; розробка методики оцінювання зниження ризиків під час оцінювання якості ПЗ [14]; розробка класифікації семантичних дефектів та основних принципів та процедур калібрування методу [15]; розробка моделі ПЗ як об’єкта експертизи, принципів контролю програмних інваріантів під час статичного аналізу коду та розробка комплексу утиліт статичного аналізу [16]; аналіз впливу диверсифікації верифікації на достовірність оцінки якості [17].

Апробація результатів дисертації. Основні положення досліджень доповідалися і обговорювалися на постійно діючому семінарі “Критичні комп’ютерні технології та системи” на кафедрі “Комп’ютерні системи та мережі” Національного аерокосмічного університету ім. М.Є.Жуковського “ХАІ”, а також на таких конференціях та симпозіумах: Другій Міжнародній міждисциплінарній науково-практичній конференції “Сучасні проблеми гуманізації та гармонізації управління” (Харківський національний університет імені В.Н. Каразіна, 2001 р.); Міжнародній науково-технічній конференції “Інтегровані комп’ютерні технології в машинобудуванні”, ІКТМ (Харків, „ХАІ” 2001–2005 рр.); Міжнародному симпозіумі „Измерения, важные для безопасности в реакторах” (Москва, Росія, 2003 – 2004 рр. та Смолянице, Словакія, 2005 р.); Дев’ятому міжнародному конгресі двигунобудівників (Харків, „ХАІ”, 2004 р.).

Публікації. Основні результати дисертації відображені у 17 роботах, серед яких 3 статті у наукових журналах, 4 статті у збірниках наукових праць, що включені до переліку фахових видань ВАК України, а також 10 тез доповідей у збірниках матеріалів наукових конференцій.

Структура роботи. Повний обсяг дисертації становить 197 сторінок, у тому числі 45 рисунків на 4 окремих сторінках, 14 таблиць на 1 окремій сторінці, список з 174 використаних літературних джерел на 18 сторінках, а також 2 додатки на 30 сторінках.

ОСНОВНИЙ ЗМІСТ РОБОТИ

У вступі обґрунтовано актуальність дисертаційної роботи, сформульовано мету та задачі досліджень, наукову новизну і практичну значущість отриманих результатів.

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

Сформульована загальна наукова задача дисертації декомпозована на ряд часткових задач, що пов’язані з розробкою методів незалежної верифікації ПЗ.

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

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

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

Запропоновано та досліджено властивості семантичної алгебри (табл. 1), що визначає аксіоматику семантичного відображення, та правила перетворень семантик і семантичні умови коректності операторних відображень.

Рис. 2. Структура семантичного простору у базисі Час, Довжина, Маса

Таблиця

Аксіоматика семантичного відображення

№ | Операторна

конструкція | Семантичне

відображення | Умова семантичної коректності

1 | А=В |

U(s)=A(s) |

A(s)=B(s) Збіг семантичних векторів

2 | А±В

3 | А > В

4 | А < В

3 | А*В | U(s)=A(s)+B(s) | Завжди

4 | А/В | U(s)=A(s)-B(s)

5 | АN | U(s)=NA(s) | N(s)=0 відсутність розмірності показника степеня

Подальшим розвитком семантичного вектора є семантичне число зі структурою: де — кількісна характеристика, а – семантичний вектор програмної змінної, що характеризує її фізичний тип. Аксіоматику розширеної семантичної алгебри подано у табл.2.

Таблиця

Операції над семантичними числами

№ | Операція | Мат. запис | Результат | Умова виконання

1 | Складання | Z=X+Y | Z0=X0+Y0 | Xi=Yi , i 0

2 | Віднімання | Z=X-Y | Z0=X0-Y0 | Xi=Yi i 0

3 | Множення | Z=X*Y | Z0=X0*Y0 Zi=Xi + Yi—

4 | Ділення | Z=X/Y | Z0=X0/Y0 Zi=Xi - Yi—

5 | Піднесення до степеня | Z=Xn | Z0=X0n Zi=Xi * n | ni=

6 | Порівняння | X op Y | X op Y, де op — операція порівняння | Xi=Yi i 0

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

Метрика семантичного простору: ,, визначає відстань між елементами: . Це дозволяє верифікувати ПЗ не тільки за збігом значень (їх приналежністю -довкілля еталонних значень), але і за фізичним типом, що визначається збігом семантичних складових. При цьому необхідною умовою семантичної коректності ПЗ є а достатньою умовою існування семантичних програмних дефектів , що обчислюються для семантичних векторів лівих та правих операндів для всіх адитивних операцій. Це дозволяє з точністю до виразу визначати семантичні дефекти, класифікацію яких наведено у табл. 3, у якій прийняті такі позначення: Dimfi, Dimri – фактична та необхідна розмірності першого та другого операндів; „+” –дефект виявляється ; „–” – дефект не виявляється ; „?” – можливе виявлення дефекту.

Модель дефектів ПЗ, зображена на рис. 3, припускає спотворення як операндів та операцій. Ефективність методу , де , – ймовірності виявлення та відсутності семантичного дефекту, визначається складом арифметичних операцій та семантичних інваріантів за формулою: , де – ймовірність адитивних операцій у коді; – ймовірність відсутності дефектів у коді, – ймовірність збігу семантик під час дефекту – , де – семантично еквівалентні частки даних.

Таблиця

Класифікація семантичних дефектів

Команда | Операнди

Dimf1=Dimr1 | Dimf1 Dimr1

Dimf2=Dimr2 | Dimf2Dimr2 | Dimf2=Dimr2 | Dimf2Dimr2

Норма | Дефект | Дефект | Дефект | Дефект

Адитивна | Складання та відні-мання | Норма | Норма | - | + | + | +

ААрифм.Адитивні | - | - | + | + | +

ААрифм.Мульт. | + | + | + | + | +

Порівняння
(С) | Норма | Норма | - | + | + | +

САрифм.Адитивні | - | - | + | + | +

САрифм.Мульт. | + | + | ? | ? | ?

СС | - | - | + | + | +

Присвоєння | Норма | Норма | - | + | + | +

Виклик

Функ-ції Процедури | Спотворення пар-ра | Норма | - | + | + | +

Спотворення назви функції | ? | ? | ? | ? | ?

Мультиплі-катив-на | Множення

Ділення

Піднесення до степеня | Норма | Норма | - | + | + | +

МАрифм. Адитивні | + | ? | ? | ? | ?

МАрифм.Мульт. | + | + | ? | ? | ?

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

Сім’ї ліній зверху–вниз мають ймовірності збігу семантик Рт ={0.; 0.25; 0.5; 0.75; 1}, для кожної з сімей лінії зверху-вниз мають ймовірності адитивних операцій Ра={0; 0.25; 0.5; 0.75; 1}. Ефективність методу зростає зі зменшенням ймовірності програмних дефектів для Рт>0.25, а для Рт=0, тобто при дуже великій кількості використаних типів, не опускається нижче 0.9.

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

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

У третьому розділі узагальнено результати розділу 2 для побудови технології незалежної верифікації та експертизи ПЗ. На рис. 5 визначено базові процедури методу верифікації ПЗ ІУС: нормалізація об’єкта експертизи; інструментування програмного коду для побудови семантичної моделі ПЗ; вимірювання покажчиків експертизи; калібрування семантичної моделі відносно статистичних характеристик ПЗ; обробка результатів та оцінювання характеристик якості.

Рис. 5 Метод верифікації ПЗ, заснований на семантичних інваріантах

Кожна з процедур подана у вигляді досить простих операцій та реалізується окремою утилітою.

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

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

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

Калібрування семантичної моделі дозволяє оцінити вплив статистичних характеристик програмного коду на достовірність незалежної верифікації. Набув подальшого розвитку адаптивний метод калібрування ефективності, що визначає чутливість та ступінь різноманіття диверсного методу верифікації, шляхом ін’єкції дефектів у семантичну модель ПЗ згідно з профілем проекту, який виключає “інтерференцію” та породження вторинних дефектів в адресному просторі, завдяки суміщенню ін’єкції дефектів, вимірювання атрибутів програмних інваріантів та виявлення дефектів. Достовірність верифікації визначається часткою знайдених дефектів серед тих, що були ін’єктовані.

Обробка результатів та оцінка характеристик якості здійснюються на підставі результатів попередніх етапів. Загальна оцінка коректності, у разі невиявлення програмних дефектів, формується як виважена сума локальних достовірностей окремих програмних модулів. Як вагові коефіцієнти використовуються кількості операцій у модулях. Удосконалено метод оцінки результату диверсної технології верифікації шляхом обґрунтування кількісного вимірювання тенденцій та прогресу – “зниження ймовірності залишкових дефектів” з урахуванням незалежної верифікації програмного забезпечення інформаційно-управляючих систем.

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

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

Апробація методу і розробленого інструментального засобу виконана під час незалежної верифікації ПЗ: ПТК системи автоматичного регулювання реакторного відділення ПТК САР-4 РО; системи керування перевантажувальної машини типу МПС-В-1000Z2-3-У4.2 енергоблоку №2 Запорізької АЕС; систем сигналізації аварійного захисту (СІАЗ) та регуляторів обмеження потужності (РОМ) для 1-го та 2-го блоків Ровенської АЕС розробки АТ НВО „ХАРТРОН”.

В перелік функціональних алгоритмів, що аналізувалися, було включено алгоритми обробки вхідної інформації; інформаційно-логічні схеми режимів роботи та алгоритми організації обчислювального процесу. Загалом 283 файли мовою С++. Семантичних дефектів не виявлено. Загальна кількість адитивних операцій в модулях —20766, мультиплікативних— 1581. Загальна кількість семантичних типів у програмному продукті — 11. Середня ймовірність випадкового збігу фізичних типів – 0.07.

Діапазон достовірності семантичної верифікації – (0.84;0.95). Загальна достовірність результатів верифікації, що обчислювалася як зважена сума з ваговими коефіцієнтами — кількостями операцій у модулях, для програмного проекту склала 0.86. Таким чином, ймовірність існування у програмному продукті залишкових семантичних дефектів всіх класів було зменшено у сім разів. Що дозволяє з високою достовірністю стверджувати про високу якість програмного продукту.

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

У додатку наведено програмні коди основних модулів інтегрованого інструментального середовища підтримки експертизи та незалежної верифікації, а також акти впровадження результатів дисертаційної роботи.

ВИСНОВКИ

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

При цьому одержані такі наукові та практичні результати:

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

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

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

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

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

6. У результаті дослідної експлуатації було експериментально оцінено розроблено методи підвищення надійності програмного забезпечення. Доведено ефективність моделей та методів під час сертифікаційних випробувань. Досягнуто зменшення ймовірності існування залишкових семантичних програмних дефектів у сім разів.

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

СПИСОК ОПУБЛІКОВАНИХ ПРАЦЬ ЗА ТЕМОЮ ДИСЕРТАЦІЇ

1. Харченко В.С., Манжос Ю.С., Петрик В.Л. Статистический анализ программного обеспечения системы управления космическим аппаратом и оценка проверяющей способности семантического контроля // Технология приборостроения.— 2002. № 2.— С. –59.

2. Манжос Ю.С. Оценка эффективности независимой верификации программного обеспечения // Авіаційно-космічна техніка і технологія.— 2004. – № 7.–С.210–214.

3. Конорев Б.М., Засуха С.А., Манжос Ю.С., Семенов Л.П., Сергиенко В.В., Харченко В.С., Чертков Г.Н. Модель оценивания качества программного обеспечения ИУС критического применения на основе инвариантов // Радіоелектронні і комп’ютерні системи. — 2006.—№7(19).–С.162–170.

4. Манжос Ю.С. Типізація даних у системах критичного застосування // Системи обробки інформації. –Харків: Харківський військовий університет, 2002.— Вип.3(19).— С.54–57.

5. Харченко В.С., Шостак И.В., Манжос Ю.С. Принципы построения интеллектуальной системы сертификации программного обеспечения // Системи обробки інформації.–Харків: Харківський військовий університет, 2002.— Вип.4(20). — С.3–7.

6. Манжос Ю.С. Принципы семантического контроля программного обеспечения // Авіаційно-космічна техніка і технологія. — Харків: Нац. аерокосм. ун-т „Харк. авіац. ін-т”, 2002. — Вип. . — С. 307–315.

7. Манжос Ю.С. Семантический контроль программного обеспечения систем критического применения // Авіаційно-космічна техніка і технологія.— Харків: Нац. аерокосм. ун-т „Харк. авіац. ін-т”, 2002.— Вип. 34. – С. 207–212.

8. Манжос Ю.С. Методи підвищення якості програмного забезпечення // 2-го Міжнародна міждисциплінарна науково-практична конференція “Сучасні проблеми гуманізації та гармонізації управління”. – Харків: Харківський національний університет, 2001. — С.134-135.

9. Манжос Ю.С. Методи підвищення якості программного обеспечения РКТ // Міжнародна науково-технічна конференція “Інтегровані компьютерні технології в машинобудуванні”.— Харків: Нац. аерокосм. ун-т “Харк. авіац. ін-т”, 2001.— С.120.

10. Конорев Б.М., Манжос Ю.С., Харченко В.С., Чертков Г.Н. Семантический метод независимой верификации программного обеспечения информационно-управляющих систем важных для безопасности АЭС // Международный симпозиум “Измерения, важные для безопасности в реакторах”. – Москва: Институт проблем управления им.Трапезникова, 2003. –С.10-1–10-14.

11. Манжос Ю.С., Петрик В.Л. Семантические пространства ИУС с интенсивным использованием программного обеспечения // Міжнародна науково-технічна конференція “Інтегровані комп’ютерні технології в машинобудуванні”.—Харків: Нац. аерокосм. ун-т „Харк. авіац. ін-т”, 2003. – С.277.

12. Клименко Т.А., Манжос Ю.С. Динамическая экспертная система оценки программного обеспечения // Міжнародна науково-технічна конференція “Інтегровані комп’ютерні технології в машинобудуванні”.—Харків: Нац. аерокосм. ун-т „Харк. авіац. ін-т”, 2003. — С.276.

13. Конорев Б.М., Харченко В.С., Чертков Г.Н., Алексеев Ю.Г., Манжос Ю.С., Методология и интегрированная инструментальная среда поддержки экспертизы и независимой верификации программного обеспечения ИУС // Межд. симпозиум “Измерения, важные для безопасности в реакторах”. – Москва: Институт проблем управления им.Трапезникова, 2003. — С.12-1 – 12-2.

14. Конорев Б.М., Алексеев Ю.Г., Манжос Ю.С., Сергиенко В.В., Харченко В.С., Чертков Г.Н. Риск-ориентированный подход к оценке качества ПО ИУС важных для безопасности АЭС с учетом независимой верификации // Межд. симпозиум “Измерения, важные для безопасности в реакторах”. – Москва: Институт проблем управления им.Трапезникова, 2004.— С.16-1–16-12.

15. Конорев Б.М., Алексеев Ю.Г., Клименко Т.А., Манжос Ю.С., Петрик В.Л., Сергиенко В.В., Харченко В.С., Чертков В.С. Калибровка чувствительности методов статического анализа, используемых для оценки качества и безопасности ПО ИУС АЭС // Межд. симпозиум “Измерения, важные для безопасности в реакторах”. – Москва: Институт проблем управления им.Трапезникова, 2004. —С.15-115-12.

16. Конорев Б.М., Алексеев Ю.Г., Брылев А.А., Брюханков С.С., Манжос Ю.С., Сергиенко В.В., Харченко В.С., Чертков Г.Н. Оценивание качества ПО ИУС критического применения: утилиты семантического и интервально- точностного анализа исходного кода // Международный симпозиум „Измерения важные для безопасности реакторов” Пятое собрание. — Смоленице: Словацкое Научно-техническое общество, 2005.—C.XI-1/8–XI-8/8.

17. Конорев Б.М., Алексеев Ю.Г., Манжос Ю.С., Сергиенко В.В., Харченко В.С., Чертков Г.Н. Оценивание качества ПО ИУС критического применения: Диверсификация технологий верификации // Международный симпозиум „Измерения важные для безопасности реакторов” Пятое собрание. Смоленице: Словацкое Научно-техническое общество, 2005. —С.Х-1/11-Х–11/11.

АНОТАЦІЯ

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

Дисертація на здобуття наукового ступеня кандидата технічних наук за спеціальністю 05.13.06 – автоматизовані системи управління і прогресивні інформаційні технології. – Національний аерокосмічний університет ім. М.Є. Жуковського “Харківський авіаційний інститут”, Харків, 2006.

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

Ключові слова: семантичний простір, семантична модель, незалежна верифікація, калібрування, експертиза, сертифікація .

АННОТАЦИЯ

Манжос Ю.С. Семантические модели, методы и информационная технология повышения надежности программного обеспечения информационно-управляющих систем. – Рукопись.

Диссертация на соискание научной степени кандидата технических наук по специальности 05.13.06 – автоматизированные системы управления и прогрессивные информационные технологии. – Национальный аэрокосмический университет им. Н.Е. Жуковского “Харьковский авиационый институт”, Харьков, 2006.

Диссертация посвящена повышению эффективности экспертизы и сертификации программного обеспечения информационно-управляющих систем критического применения с помощью разработки моделей и инструментальных средств, обеспечивающих независимую семантическую верификацию на основе анализа сохранения на всех проектных уровнях программного инварианта—семантики программных переменных.

Введено понятие семантического пространства, элементами которого являются физические типы данных. Семантическое пространство — линейное метрическое пространство, базисом которого являются основные единицы выбранной системы единиц, а элементами пространства – размерности физических величин. Одному и тому же элементу пространства может соответствовать несколько программных переменных, имеющих одну размерность (семантику). Для системы СИ базис семантического пространства включает: метр; килограмм; секунду; Ампер; Кельвин; канделу; моль; радиан; стерадиан. На осях координат откладываются показатели степени. В связи с тем, что все физические типы в системе СИ имеют размерности, выражающиеся целочисленными показателями степеней базовых единиц, элементы семантического пространства также будут иметь целочисленные координаты, а само пространство будет дискретным. Операции над элементами СП выполняются по законам векторной алгебры, а семантическое пространство является линейным и векторным.

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

Разработан метод построения семантической моделей ПО. Обосновано использование моделей независимой верификации. Выполнена вероятностная оценка достоверности независимой верификации, основанной на семантических инвариантах. Доказана зависимость проверяющей способности метода от статистических характеристик ПО: операционного состава и семантического состава данных.

Предложен метод независимой верификации, который положен в основу автоматизированного рабочего места эксперта Сертификационного центра АСУ Государственного центра качества Государственного комитета ядерного регулирования Украины. Определены порядок, взаимосвязь и состав основных процедур независимой верификации.

Нормализация объекта экспертизы – подготовительная процедура при экспертизе. Включает работы по регистрации объекта экспертизы в БД утилит оценки качества, формированию списков исходных файлов и технической документации и синтаксическому разбору исходного кода, выполняемому для оценки возможности дальнейшего анализа. Результатом является построение синтаксической модели.

Инструментирование исходного ПО – базовая процедура для дальнейших работ по оценке качества. Завершается построением семантической модели, отличающейся от исходного программного кода тем, что исходные типы данных переопределены на специальные классы, обеспечивающие при измерении возможность контроля семантических инвариантов, а при калибровке — инъекцию программных дефектов. По завершении построения семантической модели эксперт вводит характеристики программных инвариантов и определяет сигнатуры функций, не имеющих исходного кода, для контроля корректности их использования.

Измерение показателей экспертизы осуществляется посредством статического анализа контролируемых программных модулей, а также формирования данных о семантической корректности операторных отображений посредством интерпретации семантической модели и контроля семантических инвариантов.

Разработан метод оценки достоверности независимой верификации — калибровка семантической модели, в основе которой – инъекция программных дефектов в семантическую модель в соответствии со статистическими характеристиками программного кода и профилем дефектов. Отношение количества обнаруженных и инъектированных дефектов определяет достоверность метода.

Обработка результатов и оценка характеристик качества выполняется на основании оценок достоверности результатов верификации для каждого из модулей. Общий результат – нормированная взвешенная сумма локальных достоверностей, весовые коэффициенты которой – количества операций в модулях.

На основании моделей, методов разработано инструментальное средство поддержки независимой верификации и экспертизы программного обеспечения информационно-управляющих систем.

Ключевые слова: семантическое пространство, семантическая модель, независимая верификация, калибровка, экспертиза, сертификация.

ABSTRACT

Manzhos Y.S. The semantic models, methods and information technology for increasing of reliability information control system software - Manuscript.

Thesis for a candidate of technical science degree by speciality 05.13.06 – automated control systems and progressive information technologies. — National Aerospace University “Kharkiv aviation institute”, Kharkіv, 2006.

The Dissertation is devoted to the rise of efficiency of examination and certification of Information Control System of critical application with help the models and tools, that assure the independent formal verification on the basis of analysis of saving at all project levels of the program invariant-semantic of software variables. A method of construction of the semantic models software is developed. The method of estimation of authenticity of independent verification-calibration of method is developed. The main idea of calibration is the injection of program defects in the semantic model of object of examination in accordance with the statistical descriptions of program code. Architecture of tool of support of independent verification and examination of the software based systems of the critical setting is developed.

Keywords: semantic space, semantic model, independent verification, calibration, examination, certification.

Відповідальний за випуск М.О. Латкін

Підписано до друку 11.01.2007

Облік.-вид. арк. 1,0. Безкоштовно. Тираж 100 прим.

Замовлення №

____________________________________________________________

Національний аерокосмічний університет
ім. М.Є. Жуковського“

Харківський авіаційний інститут”

61070 Харків-70, вул. Чкалова, 17

Видавничий центр “ХАІ”

61070 Харків-70, вул. Чкалова, 17

izdat@khai.edu