NAU Harvester System
PROOF INDEPENDENT VERIFICATION AND FORECASTING OF THE HIDDEN DEFECTS OF CRITICAL SOFTWARE BASED MEASUREMENT DIVERSITY INVARIANTS
Наукові журнали Національного Авіаційного Університету
View Archive Info| Field | Value | |
| Title |
PROOF INDEPENDENT VERIFICATION AND FORECASTING OF THE HIDDEN DEFECTS OF CRITICAL SOFTWARE BASED MEASUREMENT DIVERSITY INVARIANTS
ДОКАЗАТЕЛЬНАЯ НЕЗАВИСИМАЯ ВЕРИФИКАЦИЯ И ПРОГНОЗИРОВАНИЕ СКРЫТЫХ ДЕФЕКТОВ КРИТИЧЕСКОГО ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ НА БАЗЕ ДИВЕРСНОГО ИЗМЕРЕНИЯ ИНВАРИАНТОВ ДОКАЗОВА НЕЗАЛЕЖНА ВЕРИФІКАЦІЯ ТА ПРОГНОЗУВАННЯ ПРИХОВАНИХ ДЕФЕКТІВ КРИТИЧНОГО ПРОГРАМНОГО ЗАБЕЗПЕЧЕННЯ НА БАЗІ ДИВЕРСНОГО ВИМІРЮВАННЯ ІНВАРІАНТІВ |
|
| Creator |
Конорев, Борис Михайлович; Національний аерокосмічний університет ім. М.Є. Жуковського “ХАІ”
Сергієнко, Володимир Володимирович; Сертифікаційний центр АСУ ДП Держцентрякості, м. Харків. Туркін, Ігор Борисович; Національний аерокосмічний університет ім. М.Є. Жуковського “ХАІ” |
|
| Subject |
Software; verification formal methods; testing; independent verification; invariant; calibration profile defects.
004.052.42 Программное обеспечение; формальные методы верификации; тестирование; независимая верификация; инвариант; калибровки; профиль дефектов. 004.052.42 Програмне забезпечення; формальні методи верифікації; тестування; незалежна верифікація; інваріант; калібрування; профіль дефектів. 004.052.42 |
|
| Description |
Dependability and Safety of instrumentation and control critical systems depend on characteristics of quality of the software, performing critical functions. Latent faults (faults undetected during testing or verification) of the critical software are factors of the risk of system failure. The independent verification of the critical software, which confirms a performance of declared functions and estimates a probability of latent faults existence, is the necessary condition according to the regulative requirements for different areas (IAEA, ESA and so on). From this point of view, the main problems are: the reliability of independent verification; assessment of latent faults probability; completeness of test coverage for the critical software and as result the quantitative assessment of functional safety. Considered is the development and implementation of the advanced methodology of proven independent verification on the base of the software sourcecode static analysis. Methodology is aimed at the assessment of the semantic, intervalprecision, logic and others invariants ((software properties invariable during the life cycle)) of critical software and also generation and presentations of results of assessment conformity to requirements of standards and project specifications.
Надежность и безопасность информационно-управляющих систем критического использования существенно зависят от качества программного обеспечения (ПО), реализующего критические функции систем. Скрытые дефекты (дефекты, не выявленные при тестировании и верификации) критического ПО являются факторами риска отказа системы. Независимая верификация критического ПО, которая подтверждает выполнение заявленных функций и дает оценку вероятности наличия скрытых дефектов, является необходимым условием нормативных требований для различных отраслей (МАГАТЭ, Европейское космическое агентство). В этом контексте основными проблемами являются: надежность независимой верификации, оценка вероятности скрытых дефектов, полнота тестового покрытия для критического ПО и как результат количественная оценка функциональной безопасности. Рассматривается разработка и использование усовершенствованной методологии доказательной независимой верификации на базе статического анализа исходных текстов ПО для оценки семантических, интервально-точностных, логических и др. инвариантов ПО (свойств ПО, остающихся неизменными по определению в течение жизненного цикла) критического ПО, а также формирование и представление результатов оценки соответствия ПО требованиям стандартов и спецификаций проекта. Надійність та безпека інформаційно-керуючих систем критичного призначення суттєво залежать від якості програмного забезпечення (ПЗ), за допомогою якого виконуються критичні функції. Приховані дефекти (дефекти, що не були виявлені при тестуванні та верифікації) критичного ПЗ являються факторами ризику відмови системи. Незалежна верифікація критичного ПЗ, що підтверджує виконання заявлених функцій та дає оцінку вірогідності наявності прихованих дефектів, є необхідною умовою нормативних вимог для різних галузей (МАГАТЕ, Європейська Космічна Агенція ). З цієї точки зору основними проблемами є: надійність незалежної верифікації, оцінювання вірогідності прихованих дефектів, повнота тестового покриття для критичного ПЗ та, як результат, кількісна оцінка функціональної безпеки. Розглядається розробка та використовування вдосконаленої методології доказової незалежної верифікації на базі статичного аналізу вихідних текстів ПЗ для оцінювання семантичних, інтервально-точностних, логічних та інших інваріантів (властивостей ПЗ, які залишаються незмінними по визначенню протягом життєвого циклу ПЗ) критичного ПЗ, а також формування і подання результатів оцінки відповідності ПЗ вимогам стандартів і специфікацій проекту. |
|
| Publisher |
National Aviation University
|
|
| Contributor |
—
— — |
|
| Date |
2011-12-10
|
|
| Type |
—
— — |
|
| Format |
application/pdf
|
|
| Identifier |
http://jrnl.nau.edu.ua/index.php/IPZ/article/view/3050
|
|
| Source |
Інженерія програмного забезпечення; Том 5, № 1 (2011); 5
Engineering Software; Том 5, № 1 (2011); 5 Инженерия программного обеспечения; Том 5, № 1 (2011); 5 |
|
| Language |
en
|
|