ДОКАЗОВА НЕЗАЛЕЖНА ВЕРИФІКАЦІЯ ТА ПРОГНОЗУВАННЯ ПРИХОВАНИХ ДЕФЕКТІВ КРИТИЧНОГО ПРОГРАМНОГО ЗАБЕЗПЕЧЕННЯ НА БАЗІ ДИВЕРСНОГО ВИМІРЮВАННЯ ІНВАРІАНТІВ
Ключові слова:
Програмне забезпечення, формальні методи верифікації, тестування, незалежна верифікація, інваріант, калібрування, профіль дефектів.Анотація
Надійність та безпека інформаційно-керуючих систем критичного призначення суттєво залежать від якості програмного забезпечення (ПЗ), за допомогою якого виконуються критичні функції. Приховані дефекти (дефекти, що не були виявлені при тестуванні та верифікації) критичного ПЗ являються факторами ризику відмови системи. Незалежна верифікація критичного ПЗ, що підтверджує виконання заявлених функцій та дає оцінку вірогідності наявності прихованих дефектів, є необхідною умовою нормативних вимог для різних галузей (МАГАТЕ, Європейська Космічна Агенція ). З цієї точки зору основними проблемами є: надійність незалежної верифікації, оцінювання вірогідності прихованих дефектів, повнота тестового покриття для критичного ПЗ та, як результат, кількісна оцінка функціональної безпеки. Розглядається розробка та використовування вдосконаленої методології доказової незалежної верифікації на базі статичного аналізу вихідних текстів ПЗ для оцінювання семантичних, інтервально-точностних, логічних та інших інваріантів (властивостей ПЗ, які залишаються незмінними по визначенню протягом життєвого циклу ПЗ) критичного ПЗ, а також формування і подання результатів оцінки відповідності ПЗ вимогам стандартів і специфікацій проекту.Посилання
Конорев Б.М. Инварианто-ориентированная оценка качества программного обеспечения космических систем/ Конорев Б.М., Харченко В.С., Алексеев Ю.Г., Манжос Ю.С., Сергиенко В.В., Чертков Г.Н. / Монография. Под ред. Конорева Б.М., Харченко В.С. – Харьков: ГП Госцентркачества, Национальный аэрокосмический университет им. Н.Е. Жуковского «ХАИ», 2009. – 224 с.
Кларк Э.М. Верификация моделей программ: Model Checking / Э.М. Кларк, О. Грамберг, Д. Пелед Пер. с англ. / Под ред. Р. Смелянского. — М.: МЦНМО, 2002. – 416 с.
Конорев Б.М., Сергиенко В.В., Новы Л., Чертков Г.Н. Калибровка методов измерения инвариантов критического программного обеспечения: профиль инъектируемых тестовых дефектов// Радіоелектронні і комп’ютерні системи. Науково-технічний журнал №6 (25), Харків, "ХАІ" 2008. – с.161 – 167 (ISSN 1814-4225).
IEC 60880 ed2:2006. Nuclear power plants – Instrumentation and Control systems important for safety – Software aspects for computer-based systems performing category А functions.
IEC 62138:2004. Nuclear power plants – Instrumentation and Control systems important for safety – Software aspects for computer-based systems performing category B and C functions.
