Скрытые дефекты программного обеспечения (ПО) информационно управляющих систем (ИУС), связанных с безопасностью (в сферах атомной энергетики, космической отрасли, авиации и др.), являются факторами рисков аномального функционирования ИУС и возникновения критических и аварийных ситуаций. Вероятность скрытых дефектов и полнота тестового покрытия критического ПО являются важными параметрами при risk-informed подходах к регулированию безопасности.

В объемах квалификационных испытаний ИУС и ПО критического назначения международной нормативной базой (стандартами МАГАТЭ, ECSS, ISO/IEC и др.) установлена необходимость обязательного проведения доказательной независимой верификации (ДНВ) критического ПО с использованием принципа разнообразия для обеспечения высокой (контролируемой) достоверности результатов.

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

Гипотеза для решения проблемы: ПО корректно, если подтверждается неизменность (сохранность) всех его инвариантов (Инвариант – свойство или атрибут ПО, остающееся неизменным по определению на протяжении всего жизненного цикла ПО). Детально гипотеза обоснована в монографии «Инварианто-ориентированная оценка качества программного обеспечения космических систем» (Под ред. Конорева Б.М., Харченко В.С. )

Методология:
Инварианто-ориентированная model-checking верификация , основанная на диверсифицированном измерении и контроле сохранности значений инвариантов ПО в режиме статического анализа исходных кодов ПО.

Модифицированный model-checking подход включает:
• Формирование моделей исходного ПО, ориентированных на диверсифицированное измерение групп инвариантов:
• Семантические инварианты программных переменных (физическая размерность, интервал изменения, точность представления) .
• Инварианты потока управления: сводимость потока управления, потенциальная достижимость и «живость» (востребованность) операторов .
• Использование оперативной памяти в конкретном проекте ПО: утечки памяти, повторное освобождение памяти.
• Структура потоков управления программы (логика выполнения).
• Специфические инварианты ИУС на компонентах FPGA («список чувствительности»; «гонки сигналов», отсутствие «защелок»).
• Экспериментальную калибровку чувствительности и степени разнообразия инварианто-ориентированных моделей методом посева тестовых дефектов ПО.
• Итоговую оценку вероятности скрытых дефектов и полноты тестового покрытия исходного ПО на основе обработки результатов калибровки.

Новизна и основные преимущества:
• Повышение достоверности оценок характеристик ПО за счет доказательной реализации принципов технологического разнообразия (диверсности) на основе диверсифицированного измерения семантических, интервально-точностных, логических и др. инвариантов ПО (физических или абстрактных свойств ПО, остающихся неизменными, по определению, в течение жизненного цикла);
• Прогнозирование вероятности скрытых дефектов ПО с использованием экспериментальной калибровки чувствительности и степени разнообразия диверсных методов измерения инвариантов в условиях конкретного проекта ПО, методом посева тестовых дефектов; вероятность скрытых дефектов представляет одну из важнейших (интегральных, базовых) характеристик критического ПО, оцениваемую при независимой верификации.
• Оценка полноты тестового покрытия критического ПО методом прямой и обратной трассировки подмножеств инвариантов различных категорий (типов), представленных в:
а) нормативном профиле требований ПО (спецификации ПО); б) исходных текстах ПО (реализации ПО).
• Возможность проведения независимой верификации при модернизации и доработках критического ПО непосредственно на объектах заказчика без вмешательства (останова) в технологические процессы.
• Новая целевая технология ДНВ обеспечивает возможность совершенствования risk-informed подходов к регулированию безопасности в области атомной энергетики и других сферах критической деятельности. В частности снижение и доведение до социально допустимого уровня рисков аномального функционирования ИУС АЭС и возникновения аварийных ситуаций из-за скрытых дефектов критического ПО на основе рамочных прогнозов вероятности скрытых дефектов и полноты тестового покрытия с контролируемой степенью неопределенности.

Сфера применения
Квалификационные испытания и анализ критичности в рамках программ гарантоспособности и безопасности (в соответствии с нормативной базой МАГАТЭ) организациями разработчиками систем управления, а также при сертификации программно-технических комплексов, нормативного регулировании и разрешительной деятельности для атомной, космической, траспортной отраслей и других сфер критического применения.

Апробация
Целевая технология ДНВ представлена комплексом программных утилит и методик, обеспечивающих реализацию сценария доказательной независимой верификации. Предложенные технические решения были апробированы и отработаны при выполнении проекта УНТЦ №4726 на реальных примерах исходных кодов ПО ИУС АЭС. Выполнение проекта показало пригодность и готовность технологии к адаптации для условий конкретных проектов критического ПО.
В 2013 году, совместно с  ЧАО «СНПО «Импульс» были проведены работы по адаптации «Мобильного инструментального комплекса для проверки характеристик качества критического ПО в режиме статического анализа» (далее - Мобильный инструментальный комплекс МИК) для возможности экспертизы программных кодов на языке С/С++ программно-технических комплексов, разрабатываемых на предприятии ЧАО «СНПО «Импульс». 28-29 января 2014 года были проведены испытания «МИК, подтвердившие возможность ввода МИК в опытную эксплуатацию.