Размещено на http://www.allbest.ru/

Размещено на http://www.allbest.ru/

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

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

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

УДК 004.415.5+004.05

Автореферат

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

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

05.13.06 - інформаційні технології

Петрик Валерія Леонідівна

Харків - 2009

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

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

Науковий керівник: - доктор технічних наук, професор Вартанян Василь Михайлович, Національний аерокосмічний університет ім. М.Є. Жуковського «Харківський авіаційний інститут», завідуючий кафедрою економіки та маркетингу

Офіційні опоненти: - доктор технічних наук, професор Жолткевич Григорій Миколайович, Харківський національний університет ім. В.Н. Каразіна, завідуючий кафедрою теоретичної та прикладної інформатики;

- кандидат технічних наук, старший науковий співробітник Кучук Георгій Анатолійович, Харківський університет Повітряних Сил ім. Івана Кожедуба, провідний науковий співробітник науково-дослідного відділу

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

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

Автореферат розісланий “ 4 ” листопада 2009 р.

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

верифікація програмний забезпечення інструментальний

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

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

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

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

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

Зв'язок роботи з науковими програмами, планами, темами.

Дослідження, результати яких викладено в дисертації, проводилися згідно з державним планом науково-дослідних робіт Міністерства освіти і науки України в Національному аерокосмічному університеті ім. М.Є. Жуковського на кафедрі економіки та маркетингу за держбюджетними темами Д605-47/2006 «Методологія та засоби створення систем підтримки прийняття рішень у наукоємному високотехнологічному виробництві» (ДР № 0106U001073) та Д605-31/2009 «Комплексне моделювання фінансово-економічних показників наукоємного виробництва» (ДР № 0108U009953), а також «Інтегроване інструментальне середовище підтримки експертизи і незалежної верифікації програмного забезпечення систем критичного застосування» (наказ № 69 від 12.07.2002) у рамках договору з Сертифікаційним центром АСУ Держцентрякості Державного комітету ядерного регулювання України. Особистий внесок автора в зазначених НДР, як співвиконавця, полягає в розробці моделі та методу незалежної верифікації ПЗ, заснованих на використанні в умовах ресурсних обмежень і неповноти проектної документації цілочисельних семантичних дескрипторів для інструментальної системи підтримки експертизи і незалежної верифікації ПЗ, що склали основу автоматизованого робочого місця експерта сертифікаційного центру, а також реалізації в реальному часі дескрипторного динамічного контролю семантичної коректності обчислювальних процесів.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

– Сертифікаційному центрі АСУ Держцентрякості Державного комітету ядерного регулювання України під час розробки «Інтегрованого інструментального середовища підтримки експертизи і незалежної верифікації програмного забезпечення систем критичного застосування» (акт впровадження від 26.12.2007);

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

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

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

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

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

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

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

Апробація результатів дисертації. Основні положення досліджень доповідалися й обговорювалися на таких конференціях: Міжнародна науково-практична конференція «Інформаційні технології: наука, техніка, технологія, освіта, здоров'я» (Харків, 2003 р.), Міжнародна науково-технічна конференція «Інтегровані комп'ютерні технології в машинобудуванні» ІКТМ (Харків, 2003-2008 р.).

Публікації. Основні результати дисертації відображено в 16 роботах, з яких 9 статей у наукових виданнях, що входять у перелік ВАК України (5 статей у науково-технічних журналах, 4 статті у збірниках наукових праць), 7 - у матеріалах конференцій.

Структура роботи. Дисертація має вступ, чотири розділи, висновки й додатки. Повний обсяг дисертації складає 198 сторінок, у тому числі 5 рисунків на 5 окремих сторінках і 25 рисунків по тексту, 2 таблиці на 4 окремих сторінках і 15 таблиць по тексту, 2 додатка на 27 сторінках, список з 154 використаних літературних джерел на 16 сторінках.

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

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

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

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

Основні результати надруковано в роботах [1, 10].

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

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

– лінійність цілочисельного дескрипторного відображення, що дозволила використовувати статичний аналіз для експертизи ПЗ при незалежній верифікації;

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

При розробці дескрипторної моделі було проаналізовано:

– системи одиниць, що дозволило оцінити вплив обраної системи одиниць на достовірність і ресурсоємність семантичної незалежної верифікації ПЗ;

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

Вибір системи одиниць впливає на достовірність семантичної незалежної верифікації ПЗ. Доведено, що достовірність семантичної незалежної верифікації залежитьвід загальної кількості фізичних величин N в системі одиниць і кількості множин

фізичних величин М, що мають еквівалентні фізичні розмірності:

Показано, що достовірність семантичної верифікації, заснованої на використанні СІ, вище на 30% порівняно із системами одиниць СГС, МКГСС, а СГС - найменш ресурсоємна.

Доведено можливість побудови стискаючого семантичного відображення n-мірного семантичного простору P на впорядковану множину скалярних числових елементів - семантичних дескрипторів S:P>D, де S - стискаюче семантичне відображення, D={d_i} - упорядкована множина семантичних дескрипторів (рис. 1).

Стискаюче семантичне відображення S, з математичної точки зору, - скалярний добуток семантичного вектора, що є елементом семантичного простору, на вектор стискаючого семантичного відображення:

де n - кількість основних

одиниць обраної системи одиниць; x_j - степінь основних одиниць фізичної розмірності,

a_j - координата вектора стискаючого семантичного відображення, яку далі будемо

називати коефіцієнтом, d - семантичний дескриптор.

Реалізація стискаючого семантичного відображення можлива при обмеженні множини елементів семантичного простіру. Діапазони модулів степенів основних одиниць становлять: для СІ L_minj = 1, L_{max j} = 7; для CГС L_minj = 1/2, L_maxj = 3; для МКГС L_minj = 1, L_maxj = 6. Необхідна умова ізоморфізму стискаючого семантичного відображення виражається як

де , a_j>0

На підставі необхідної умови ізоморфізму стискаючого семантичного відображення, обраного порядку основних одиниць СІ, діапазону модулів степенів основних одиниць визначені значення коефіцієнтів стискаючого відображення (табл. 1).

Таблиця 1. Коефіцієнти стискаючого семантичного відображення і структура семантичних дескрипторів

№ розряду	Основна одиниця	Степінь основної одиниці	Порядок розряду	Коефіцієнти стискаючого семантичного відображення aj
		xj	Розмірність
0	Знаковий розряд	1
1 2 3	Довжина [м]	4 2 1	м4 м2 м1	1/2 1/4 1/8	1/8
4	Розділовий	1/16
5 6 7	Маса [кг]	4 2 1	кг4 кг2 кг1	1/32 1/64 1/128	1/128
8	Розділовий	1/256
9 10 11	Час [сек]	4 2 1	сек4 сек2 сек1	1/512 1/1024 1/2048	1/2048
12	Розділовий	1/4096
13 14 15	Сила електричного струму [А]	4 2 1	а4 а2 а1	1/8192 1/16384 1/32768	1/32768

Семантичні дескриптори утворюють дескрипторний семантичний простір D, що є лінійним простором, в якому:

I. Для d_i, d_jD однозначно визначений елемент d_kD, що відповідає сумі

d_i + d_j: d_i + d_j = d_j + d_i; d_i + (d_j + d_к ) = (d_i + d_j) + d_к; d₀ D d_i + d₀ = d_i для d_i D; d_i D (- d_i) d_i + (- d_i) = 0.

II. Для Z і d_i D d_i D:

(d_i) = ()d_i; 1d_i = d_i; ( + )d_i = d_i + d_i; (d_i + d_j) = d_i + d_j.

Метрика дескрипторного простору: (d,d)=0; (d₁,d₂)=(d₂,d₁); (d₁,d₃)(d₁,d₂)+(d₂,d₃) визначає відстань між будь-якими елементами d₁ і d₂ із D.

Дескрипторний простір D є нормованим з нормою p, що задовольняє умовам:

1) p(d_i) = 0 тільки, якщо d_i=d₀, де d₀ - нульовий дескриптор, що має координату 0;

2) p (d_i) = ||p(d_i) для всіх , де - число;

3) p(d_i) ? 0 при d_i ? d₀;

4) p(d_i+d_j) ? p(d_i) + p(d_j), d_i, d_j D.

Простір D - дескрипторна алгебра з аксіоматично визначеною операцією множення: (d_id_j)d_к=d_i(d_jd_к); d_i(d_j+d_к)=d_id_j+d_id_к; (d_j+d_к)d_i=d_jd_i+d_кd_i; (d_id_j)=(d_i)d_j=d_i(d_j); оскільки еD такій, що ed_i=d_ie=d_i для d_iD, то е - одиниця алгебри D.

Дескрипторний семантичний нормований простір D є нормованою алгеброю, тому що в ньому виконуються аксіоми ||e|| = 1; ||d_id_j|| ? ||d_i|| ||d_j||.

Лінійність дескрипторного семантичного простіру дозволяє контролювати семантичну коректність ПЗ завдяки властивостям операцій, наведеним у таблиці 2, з позначеннями: L, R - лівий і правий операнди, d(L), d(R) - їх дескриптори.

Таблиця 2. Аксіоматика дескрипторної алгебри

№	Операція	Позначення	Умова коректності	Дескриптор результату
1	Додавання	L+R	d(L)=d(R)	d(L)
2	Вирахування	L-R	d(L)=d(R)	d(L)
3	Множення	L.R	Відсутнє	d(L)+d(R)
4	Ділення	L/R	Відсутнє	d(L)-d(R)
5	Піднесення до степеня	LR	d(R)=0	d(L)*R
6	Порівняння	L>R, L<R, L=R	d(L)=d(R)	Відсутнє
7	Присвоювання	L=R	d(L)=d(R)	d(L)

Доведено можливість побудови цілочисельного семантичного відображення n-мірного семантичного простору на впорядковану множину скалярних цілих числових елементів - цілочисельних семантичних дескрипторів I:S>С, де I - цілочисельне семантичне відображення, S - семантичний простір, С={С_i} - упорядкована множина цілочисельних семантичних дескрипторів. Цілочисельне семантичное відображення є скалярним добутком семантичного вектора на вектор цілочисельного семантичного відображення:

де f_j - коефіцієнт цілочисельного семантичного відображення, x_j - степінь основних одиниць системи одиниць (табл. 3).

Таблиця 3. Коефіцієнти цілочисельного семантичного відображення і структура цілочисельних семантичних дескрипторів

№ розряду	Основна одиниця	Степінь основної одиниці	Вага розряду	Коефіцієнти цілочисельного семантичного відображення fj
		xj	Розмірність
0 1 2	Довжина [м]	1 2 4	м1 м2 м4	1 2 4	1
3	Розділовий	8
4 5 6	Маса [кг]	1 2 4	кг1 кг2 кг4	16 32 64	16
7	Розділовий	128
8 9 10	Час [сек]	1 2 4	сек1 сек2 сек4	256 512 1024	256
11	Розділовий	2048
12 13 14	Сила электри-чного струму [A]	1 2 4	а1 а2 а4	4096 8192 16384	4096
...
31	Знаковий розряд	1

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

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

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

Стани статичного аналізатора пов'язані між собою переходами, що визначаються статистичими характеристиками - інтенсивностями: , - семантично документованих і недокументованих операндів, _A, _М, _L - адитивних, мультиплікативних і логічних операцій, _J - операцій переходу, ₁ - безумовного переходу.

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

де , -

імовірності виявлення й не виявлення семантичних дефектів ПЗ за умови їх існування, що є ймовірностями знаходження статичного аналізатора у відповідних станах. Для знаходження ймовірностей вирішена система диференціальних рівнянь Колмогорова, яка зв'язує потоки ймовірностей у кожному зі станів моделі зі змінами ймовірностей знаходження статичного аналізатора в цих станах (похідними):

(1)

Коефіцієнт семантичної повноти після підставлення знайдених ймовірностей:

(2)

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

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

Відповідно до моделі, програмний код - упорядкована множина програмних елементів, частина яких може мати дефекти ПЗ, деякі з яких можуть бути виявлені за допомогою контролю цілочисельних семантичних дескрипторів. Далі позначено: I - елемент програмної конструкції; C - команда (операція); O - операнд; N - константа; A - арифметична команда; L - логічна команда; R - команда відносини; J - команда переходу; F - виклик функції; T, T^-1 - прямі й зворотні тригонометричні функції; M - математична функція; S - системна функція; K - скалярна змінна; Q - операнд, що адресується; «+» - додавання; «-» - вирахування; «/» - ділення; «*» - множення.

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

при обмеженнях , ; [0;1]; ; Z[0;N], де i - тип елемента програмної конструкції; , - абсолютні ймовірності відповідно виявлення й невиявлення дефектів ПЗ за умови їхнього існування; P_A - частка арифметичних команд серед всіх команд; , - частка додавань і вирахувань; Z - арность операцій. Інтегрована оцінка середньої ефективності сягає 0,75.

Основні результати надруковано в роботах [2-7, 11, 14-15].

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

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

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

На рис. 6 визначено базові процедури методу незалежної верифікації ПЗ.



Рис. 6. Основні процедури методу незалежної верифікації ПЗ в умовах ресурсних обмежень і неповноти проектної документації

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

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

Основні результати надруковано в роботах [8, 9, 12, 13].

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

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

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

Математичні очікування локальних ймовірностей адитивних і мультиплікативних операцій для ПЗ «Спектр» склали 0,79 і 0,11 відповідно, дисперсії склали 0,037 і 0,034. Загальна кількість семантичних типів у програмному продукті складає 11. Середня арність операції дорівнює 2,5. Середня ймовірність випадкового збігу фізичних типів дорівнює 0,07. Діапазон локальної достовірності результатів семантичної верифікації для кожного з програмних модулів склав (0,84; 0,95). Загальна достовірність результатів верифікації програмного проекту, обчислена як зважена сума з ваговими коефіцієнтами - кількістю операндів і операцій у модулях, досягає 0,89. Таким чином, ймовірність існування в програмному продукті семантичних дефектів зменшена майже в дев'ять разів, що дозволяє з високою достовірністю стверджувати про достатній рівень ПЗ ІУС.

Основні результати надруковано в роботах [9, 12, 16].

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

ВИСНОВКИ

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

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

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

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

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

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

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

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

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

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

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

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

2. Петрик В.Л. Экспертиза программного обеспечения информационно-управляющих систем с использованием дескрипторного семантического пространства / В.Л. Петрик // Радіоелектронні і комп'ютерні системи. - 2007. - №2(21). - С.29-35.

3. Петрик В.Л. Целочисленное семантическое отображение / В.Л. Петрик // Радіоелектронні і комп'ютерні системи. - 2007. - №3(22). - С.73-81.

4. Манжос Ю.С. Оценка полноты семантического контроля программного обеспечения информационно-управляющих систем / Ю.С. Манжос, В.Л. Петрик // Авиационно-космическая техника и технология. - 2007. - № 5(41). - С. 86-93.

5. Петрик В.Л. Модель дефектов программного обеспечения / В.Л. Петрик, Ю.С. Манжос // Радіоелектронні і комп'ютерні системи. - 2008. - № 3(30). - С.46-51.

6. Конорев Б.М. Обоснование выбора системы единиц физических величин для независимой верификации при сертификации программного обеспечения / Б.М. Конорев, В.Л. Петрик // Открытые информационные и компьютерные интегрированные технологии: сб. науч. тр. Нац. аэрокосм. ун-та им. Н.Е. Жуковского «ХАИ». - Вып. 33. - Х., 2006. - С.116-120.

7. Петрик В.Л. Сжимающее семантическое отображение / В.Л. Петрик // Системи обробки інформації: зб. наук. праць Харківського університету Повітряних Сил. - Вип. 3(61). - Х., 2007.- С. 79-82.

8. Петрик В.Л. Метод дескрипторного контроля семантической корректности программного обеспечения / В.Л. Петрик // Системи управління, навігації та зв'язку: зб. наук. праць Центр. наук.-дослід. ін-ту навігації і управління. - 2007. - Вип.4. - С.140-143.

9. Манжос Ю.С. Дескрипторный контроль программного обеспечения критического применения в реальном времени / Ю.С. Манжос, В.Л. Петрик // Зб. наук. праць Харківського університету Повітряних Сил. - Вип. 1(16) - Х., 2008. - С. 90-93.

10. Кожухов В.Д. Сучасні методи верифікації програм / В.Д. Кожухов, Ю.С. Манжос, В.Л. Петрик // Інформаційні технології: наука, техніка, технологія, освіта, здоров'я: матеріали ХI Міжнар. наук.-практ. конф., 15-16 трав. 2003 р. - Х., 2003. - С.24.

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

12. Конорев Б.М. Калибровка чувствительности методов статического анализа, используемых для оценки качества и безопасности ПО ИУС АЭС / Б.М. Конорев, Т.А. Клименко, Ю.С. Манжос, В.Л. Петрик // Інтегровані комп'ютерні технології в машинобудуванні - ІКТМ 2004: тези допов. Міжнар. наук.-техн. конф. - Х., 2004. - С.400.

13. Петрик В.Л. Метод восстановления семантического контекста программы в условиях неопределенности / В.Л. Петрик // Інтегровані комп'ютерні технології в машинобудуванні - ІКТМ 2005: тези допов. Міжнар. наук.-техн. конф. - Х., 2005. - С 424.

14. Петрик В.Л. Оценка полноты независимой верификации в условиях неопределенных проектных спецификаций / В.Л. Петрик // Інтегровані комп'ютерні технології в машинобудуванні - ІКТМ 2006: тези допов. Міжнар. наук.-техн. конф. - Х., 2006. C. 483-484.

15. Петрик В.Л. Представление семантической информации с использованием целочисленного семантического отображения / В.Л. Петрик // Інтегровані комп'ютерні технології в машинобудуванні - ІКТМ 2007: тези допов. Міжнар. наук.-техн. конф. - Х., 2007. - C. 561-562.

16. Петрик В.Л. Применение сжимающего семантического отображения для контроля достоверности экономических расчетов / В.Л. Петрик // Інтегровані комп'ютерні технології в машинобудуванні - ІКТМ 2008: тези допов. Міжнар. наук.-техн. конф. - Х., 2008. - C. 114.

АНОТАЦІЯ

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

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

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

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

АННОТАЦИЯ

Петрик В.Л. Информационная технология верификации программного обеспечения информационно-управляющих систем на основе дескрипторной модели. - Рукопись.

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

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

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

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

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

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

Результаты исследований внедрены в Сертификационном центре АСУ Государственного центра качества Государственного комитета ядерного регулирования Украины при разработке «Интегрированной инструментальной среды поддержки экспертизы и независимой верификации программного обеспечения систем критического применения». В результате опытной эксплуатации экспериментально оценен разработанный метод верификации программного обеспечения. Доказана эффективность дескрипторной модели и метода при сертификационных испытаниях, обеспечивающая десятикратное, по сравнению с семантическим контролем, основанным на векторном представлении размерностей программных переменных, снижение уровня документированности и ресурсоемкости. Достигнуто девятикратное уменьшение вероятности существования семантических программных дефектов.

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

ABSTRACT

Petrik V.L. The information technology of verification for the information control system software based on the descriptor model. - Manuscript.

Thesis on competition of scientific degree of Candidate of Technical Science by specialty 05.13.06 - Information technologies. - National Aerospace University «Kharkiv aviation institute», Kharkіv, 2009.

The Dissertation is devoted to the elaboration the new verification method based on the using of integer descriptor as a formal imaging of physical dimension of the program variable. A method of construction of the descriptor model software is developed. The proposed method includes the models and procedure for rising of software reliability. Architecture of software tool is developed. The template library for real time descriptor checking is developed and proposed for using in the different branches. The method of estimation of result of independent verification of software is improved. Got subsequent development method of static analysis of software. Introduction of information technology in the integrated instrumental system for support of expertise and independent verification of critical software provided independent semantic verification.

...