С.М. Буденного, Санкт-Петербург); e-mail: B.sashka_84@mail.ru ФОРМИРОВАНИЕ УСЛОВИЙ КОРРЕКТНОСТИ ДЛЯ ВЕРИФИКАЦИИ СПЕЦИАЛЬНОГО ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ КОМПЛЕКСОВ РАДИОКОНТРОЛЯ Рассмотрен один из этапов верификации специального программного обеспечения (СПО) комплексов радиоконтроля (КРК) с использованием алгоритма обратного прослеживания условий корректности для аннотированной программы при проверке СПО КРК на наличие недекларированных возможностей и ошибок. <...> Достигнута требуемая достоверность верификации СПО при заданном уровне неопределенности измерений, повышена оперативность проведения верификации СПО КРК. <...> Keywords: Verification; Special software; Undeclared capabilities; Radio control complex; Algorithm Введение Перспективные комплексы радиоконтроля (КРК) военного назначения представляют собой аппаратно-программные средства, что требует особых подходов при проведении испытаний и обеспечении необходимых результатов измерений, связанных с имеющимся специальным программным обеспечением (СПО). <...> Назначение Верификация СПО КРК с использованием алгоритма обратного прослеживания условий корректности для аннотированной программы при проверке СПО КРК на наличие недекларированных возможностей и ошибок. <...> Достижение требуемой достоверности верификации СПО при заданном уровне неопределенности измерений. <...> Разработать алгоритм обратного прослеживания условий корректности для аннотированной программы. <...> Разработать процедуру преобразования VC (Verification Conditions) по правилам обратного прослеживания в соответствующие условия корректности. <...> Решение Одним из этапов при верификации СПО с использованием метода индуктивных утверждений будет формирование условий корректности по аннотированной программе. <...> Простейшим способом «Вестник компьютерных и информационных технологий» № 10, 2011 43 получения условий корректности является разбор аннотированной программы по управляющему графу (блок-схеме), при котором определяют контрольные точки с соответствующими <...>