ГОСТ Р МЭК 60880—2010
d) определение данных, которые считываются до их записи, данных, которые записываются до их чтения,
данных, записанных дважды без их промежуточного чтения:
e) проверку информационного потока по спецификации:
f) оказание помощи в проектировании плана динамических испытаний;
д) управление тестовыми данными и, возможно, генерацию тестовых данных.
Н.2.2 Программа семантической проверки
Программа семантической проверки описывает математические соотношения между выходными и вход
ными переменными для каждого семантически достижимого пути в свободных от ветвлений частях программы.
Это позволяет проводить проверку того, что программа будет делать при всех обстоятельствах, а также регистри
ровать дефекты, такие, например, как неожидаемые выходные величины, на которые влияют входные величины,
неправильный отклик на неожидаемые входные величины, неправильная последовательность функций и опера
торов и т.п.
Н.2.3 Генератор формализованных проверок
Формализованные проверки проекта требуют использования интерактивной программы, которая проводит
необходимую работу с символами под управлением оператора, для того чтобы выполнить доказательство пра
вильности. Такая программа известна как «помощник в доказательстве теорем» (ПДТ). Это обычно означает
применение программы проверки доказательств, вход по такой программе является выходом ПДТ. ПДТ пред
ставляют собой большие программы, отсутствие дефектов для которых нельзя доказать. Поэтому необходимо
проведение разносторонней верификации. Программа проверки доказательств должна быть основана на фор
мализованной теории доказательств, и эта программа должна верифицироваться по отношению к этой теории.
Н.2.4 Аниматор
По возможности, спецификации рекомендуется анимировать с тем. чтобы конечный пользователь системы
мог проверить различные аспекты спецификации или проекта с целью подтверждения соответствия (насколько
это возможно) требований спецификации и предлагаемого проекта. Анимация должна с максимальной
возмож ностью представлять проект и может потребовать использования макетов для демонстрации
нефункциональных аспектов. Эта оценка проводится на соответствие критериям пользователя, и требования к
системе могут быть модифицированы в свете этой оценки.
Н.2.5 Анализатор соответствия
Анализатор соответствия может показать, что программа правильно реализует спецификацию. При этой
демонстрации анализатор соответствия использует входные и выходные условия плюс инвариант цикла. Анали
затор соответствия систематически подтверждает выполнение в программе каждого условия.
77