РОЗДІЛ 2
СЕМАНТИЧНА МОДЕЛЬ ПРОГРАМНОГО ЗАБЕЗПЕЧЕННЯ
2.1. Модель та схема вимірювання якості ПЗ
Як було зазначено вище, сферою застосування незалежної верифікації ПЗ мають бути експертиза, сертифікація та ліцензування ПЗ ІУС критичного застосування у державних установах регулювання безпеки та якості товарів та послуг, що дозволить:
- підвищіти якість експертизи відповідності ПЗ ІУС регулюючим вимогам на підставі диверсифікації технологій верифікації за показниками "достовірність", "повнота", "трудомісткість";
- зменшити ризики аварійних ситуацій, пов'язаних із залишковими дефектами ПЗ ІУС, що є ключовим фактором забезпечення безпеки АЕС в довгострокових програмах розвитку атомної енергетики.
Повна модель якості ПЗ (згідно зі стандартами ISO/IEC 9126 [73], ISO/IEC 14598 [71] ) подана трьома моделями, що визначають на рис. 2.1:
- внутрішню якість;
- зовнішню якість;
- якість у використанні.
Така диверсифікація моделей якості призначена для оцінювання якості ПЗ у різних середовищах реалізації на базових етапах ЖЦ ІУС, таких як:
- розробка специфікацій ПЗ;
- інтеграція ПЗ;
- реалізація на реальній платформі.
Необхідною умовою забезпечення якості є можливість за допомогою відповідних методик [78] вимірювання атрибутів - физичних або абстрактних властивостей [78].
Рис. 2.1. Модель та схема вимірювання якості ПЗ
Метрика, за визначенням, це сукупність методу та шкали вимірювання атрибуту або характеристики ПЗ.
Загальна схема вимірювання якості ПЗ передбачає формування ієрархії значень "метрика (міра) - атрибут - підхарактеристика - характеристика" для всіх складових частин (ієрархії) архітектури та на їх підставі інтегральної оцінки якості конкретного програмного проекту.
База аналізу та оцінки якості проекту ПЗ являють собою суперпозицію множин атрибутів ПЗ , що визначають характеристики внутрішньої, зовнішньої якості та якості у використанні.
Пропонується доповнити модель вимірювання якості ПЗ контролем фізичних розмірностей програмних змінних, що відповідають вхідним даним та вихідним результатам.
Це дозволить підвищити надійність програмного забезпечення, тому що введений атрибут - фізична розмірність є інваріантом, а його порушення на будь-якому проектному рівні буде свідчити про порушення атрибутів якості.
2.2. Програмне забезпечення як семантичне відображення
Диверсифікація технології оцінювання якості програмного забезпечення ґрунтується на розгляді відображень семантичних характеристик вхідних змінних області визначення у відповідні характеристики вихідних змінних області значень інформаційно-управляючих систем. Модель програмного забезпечення як семантичного відображення подана на рис. 2.2.
Рис. 2.2. Модель ПЗ як семантичного відображення
Області визначення і значень семантичного відображення, що реалізує ПЗ, представлені простором, визначеним у базисі:
1. Адресний простір ПЗ, розділений на сегменти коду і даних. Сегмент коду - програмні команди. Деякі з команд можуть бути контрольними, в яких на підставі спеціально розробленої алгебри здійснюватиметься контроль збереження семантичних інваріантів. Сегмент даних - програмні змінні. Кожна із змінних має деяку семантичну характеристику (фізичну розмірність), що є інваріантом, тобто не змінюється протягом всього часу роботи ІУС та при будь-яких вхідних даних.
2. Семантика - фізічна розмірність програмної змінної (семантичний інваріант). Вісь утворена проектуванням багатовимірного семантичного простору на пряму. Різним точкам осі "семантика" відповідають різні фізичні розмірності.
Семантичні спектри - лінії, що огинають відрізки, відповідають множині значень розмірностей вхідних даних та вихідних результатів у адресному просторі ПЗ. Спектр має проекції на осі "Адреса" і "Семантика". Відрізки різної довжини відповідають різним розмірностям (семантичним інваріантам). Позиція ліній по вертикалі відповідає адресі програмної змінної. На рис. 2.2 показано два спектри: спектр вхідних даних та спектр вихідних результатів. Семантичне відображення зводиться до відображення вхідного семантичного спектру на вихідний семантичний спектр.
Для контролю семантичних інваріантів кожній скалярній програмній змінній та кожному елементу масиву ставиться у відповідність масив чисел (семантичний вектор), елементи якого відповідають проекціям фізичної розмірності програмної змінної на базис семантичного простору. Це надає можливості спростити оцінку якості ПЗ та здійснювати її за допомогою незалежної верифікації шляхом статичного аналізу коду.
2.3. Нормалізована модель програмного забезпечення
У процесі незалежної верифікації програмний проект приводиться до нормалізованої форми - ієрархії програмно-технічних комплексів (ПТК), функцій і операторів, що проектуються на адресний простір фон Неймана, як зображено на рис. 2.3.
Рис. 2.3. Нормалізована модель програмного забезпечення
Об'єкт експертизи складається з кількох ПТК, взаємодія яких умовно показана на функціональній моделі. Кожний з ПТК, відповідно до технічного завдання, виконує набір деяких функцій, взаємодія яких описується функціональними моделями. Інтерфейси всіх ПТК містять вхідні дані і вихідні результати. Кожна з програмно-реалізованих функцій ПТК є впорядкованою множиною операторів програмного коду, що функціонують у модифікованому просторі фон Неймана, побудованою у базисі: адреса елементу пам'яті та умовний час.
Весь обсяг адрес поділяється на два сегменти:
1. Сегмент даних, що містить множину програмних змінних і констант, які мають семантичні характеристики.
2. Сегмент коду, що містить множину команд програми.
Кожен з операторів програми може бути пов'язаний з декількома елементами модифікованого простору: даними (програмними змінними) і командами.
Обчислювальний маршрут при виконанні програми показаний у вигляді направленої пунктирної лінії в сегменті коду. Таким чином викон