Надійність та безпека інформаційно-керуючих систем критичного призначення суттєво залежать від якості програмного забезпечення (ПЗ), за допомогою якого виконуються критичні функції. Приховані дефекти (дефекти, що не були виявлені при тестуванні та верифікації) критичного ПЗ являються факторами ризику відмови системи. Незалежна верифікація критичного ПЗ, що підтверджує виконання заявлених функцій та дає оцінку вірогідності наявності прихованих дефектів, є необхідною умовою нормативних вимог для різних галузей (МАГАТЕ, Європейська Космічна Агенція ). З цієї точки зору основними проблемами є: надійність незалежної верифікації, оцінювання вірогідності прихованих дефектів, повнота тестового покриття для критичного ПЗ та, як результат, кількісна оцінка функціональної безпеки. Розглядається розробка та використовування вдосконаленої методології доказової незалежної верифікації на базі статичного аналізу вихідних текстів ПЗ для оцінювання семантичних, інтервально-точностних, логічних та іншихінваріантів (властивостей ПЗ, які залишаються незмінними по визначенню протягом життєвого циклу ПЗ) критичного ПЗ, а також формування і подання результатів оцінки відповідності ПЗ вимогам стандартів і специфікацій проекту.
Надежность и безопасность информационно-управляющих систем критического использования существенно зависят от качества программного обеспечения (ПО), реализующего критические функции систем. Скрытые дефекты (дефекты, не выявленные при тестировании и верификации) критического ПО являются факторами риска отказа системы. Независимая верификация критического ПО, которая подтверждает выполнение заявленных функций и дает оценку вероятности наличия скрытых дефектов, является необходимым условием нормативных требований для различных отраслей (МАГАТЭ, Европейское космическое агентство). В этом контексте основными проблемами являются: надежность независимой верификации, оценка вероятности скрытых дефектов, полнота тестового покрытия для критического ПО и как результат количественная оценка функциональной безопасности. Рассматривается разработка и использование усовершенствованной методологии доказательной независимой верификации на базе статического анализа исходных текстов ПО для оценки семантических, интервально-точностных, логических и др. инвариантов ПО (свойств ПО, остающихся неизменными по определению в течение жизненного цикла) критического ПО, а также формирование и представление результатов оценки соответствия ПО требованиям стандартов и спецификаций проекта.
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 isaimed 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.
