Методы тестирования вычислительных процессов

Немолочнов О.Ф., Зыков А.Г., Поляков В.И., Осовецкий Л.Г., Петров К.В.

МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ

ФЕДЕРАЦИИ


ФЕДЕРАЛЬНОЕ АГЕНТСТВО ПО ОБРАЗОВАНИЮ


САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

ИНФОРМАЦИОННЫХ ТЕХНОЛОГИЙ, МЕХАНИКИ И ОПТИКИ

Источник: http://books.ifmo.ru/ntv/ntv/45/ntv_45.pdf

Введение

Постоянно повышающиеся требования к качеству программных продуктов заставляют разработчиков уделять все большее внимание технологическому процессу разработки, а также вопросам тестирования и верификации программ.

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

Графо-аналитические модели

ГАМ задается в виде множества вершин: условных, описывающих ветвления по условиям предикатам, линейных, описывающих вычисление переменных по аналитическим формулам – выражениям, и дуг связи между ними. Сходящиеся дуги описываются с применением виртуальных вершин объединения дуг.

Комплексное кубическое покрытие состоит из логической части в виде покрытий и алгебраических выражений переменных. Оно строится по ГАМ на основе алгебротопологических методов.

Примитивы покрытий вершин

Примитивные вырожденные покрытия вершин ГАМ показаны на рис.1.

Покрытия объединяют в себе булевы переменные B={a, b, c ,…}, вырабатываемые по условиям предикатам АЛУ процессора в виде специальных признаков – флагов, и реализуются командами условной передачи управления (if Jump) и сигналами управления z?Z, вырабатываемыми ЦУУ и осуществляющими передачу управления от коман- ды к команде.

Так как вершины ГАМ являются по определению замкнутыми множествами [3], то множества Z можно ограничить только переменными z, осуществляющими передачу управления от вершине к вершине, т.е. убрать из рассмотрения внутренние передачи управления от команды к команде, чтобы не затенять и не усложнять излишними подробностями кубические покрытия. Заметим, что кубические покрытия являются строгим математическим описанием ГАМ любого вычислительного процесса, построенного из указанных выше трех типов вершин.

Комплексные покрытия переменных

Покрытия переменных r є R, задаваемых согласно концептуальной модели вы- числительного процесса [4] в виде итеративных и рекуррентных формул и выражений, строятся путем перебора путей по ГАМ от точки Tin до точки Tout или наоборот и пересечения конкретных примитивных покрытий вершин, входящих в рассматриваемый путь. Если в процессе перебора путей встречаются противоречия, т.е. кубы из примитивов дают пустое пересечение, то данный куб просто удаляется из покрытия.

Методы верификации

Общая схема верификации показана на рис.2.

Здесь рассмотрен случай, когда один и тот же вычислительный процесс реализован двумя различными способами. На схеме показано, что на основании технических заданий (ТЗ) или разработанных программ строятся ГАМ и комплексные покрытия двух рассматриваемых вычислительных процессов. Из них исключаются значения, на которых функция не определена (don't care), методом алгебро-топологического вычитания, и строятся контролирующие тесты. Предложены два способа верификации этих процессов:

• метод алгебро-топологического вычитания покрытий каждого из каждого. При условии пустого значения результата делается заключение о эквивалентности данных вычислительных процессов;
• метод построения тестовых наборов по комплексным покрытиям путем пересечения кубов из интервальных частей покрытий и перекрестного тестирования, по результатам которого делается заключение о результатах верификации. Различия вычислительных процессов могут порождаться:

• различными покрытиями одних и тех же множеств предикатов;
• различием их функциональной декомпозиции, что может быть обусловлено выбором начального условия;
• проектированием программ на различных алгоритмических языках и различными трансляторами;
• различием аналитических выражений для вычисляемых переменных, формулы для которых подвергнуты преобразованиям с целью их упрощения или, например, с целью минимизации погрешности вычислений.

При проведении верификации по покрытиям следует учитывать следующие факторы:

• компенсацию условий предикатов;
• эквивалентность, т.е. размножение некоторых условий;
• несуществующие значения (don’t care), возникающие в ходе функциональной декомпозиции неполностью определенных функций.

Указанные факторы вызывают основные затруднения в алгоритмизации и построении САПР верификации.

Пример верификации ациклического процесса

Пусть задана некоторая интервальная формула:
реализующая вычисления некоторой переменной r по различным формулам: FR1, FR2 и FR3 произвольного вида в зависимости от двух булевых переменных, задающих не- которые условия предикаты в виде неравенств: a: x<=k1; b: x>=k2.

Переход от неравенств к булевым переменным при проектировании вычислительного процесса позволяет абстрагироваться от конкретного смысла неравенств и соответст- вующих им условий предикатов и рассмотреть решение задачи верификации в общем виде. Графо-аналитические модели вычисления переменной r приведены на рис. 3. На рис. 3а показана функциональная декомпозиция булевой функции f=f(a,b) с начальной вершиной условия предиката а (ГАМ 1), а на рис. 3б – с начальной вершиной b (ГАМ 2).

Построим комплексные кубические покрытия C1(r) и C2(r) для вычисляемой переменной r по ГАМ 1 и ГАМ 2: По покрытиям C1(r) и C2(r) построим тесты Т1(r) и Т2(r) путем пересечения кубов из интервальных частей покрытий C1(r) и C2(r), соответственно. Получим тесты: Заметим, что для формул должны выполняться условия: /FR1/<>/FR2/<>/FR3/<>p, т.е. вычисляемые и хранимые значения должны различаться на разных наборах теста. Штрихами в тестах отмечены значения активно изменяемых условий-предикатов.

С учетом удаления ab=11 верификация по покрытиям дает C1# C2 = 0 и C2# C1 = 0, что и свидетельствует об эквивалентности вычислительных процессов. Это наглядно можно наблюдать на картах Карно, приведенных на рис.3.

Перекрестное тестирование дает следующий результат: R1(T1)=R2(T1) и R1(T2)=R2(T2) , что также подтверждает эквивалентность вычислительных процессов. Заметим, что если переменную r вычислять по разным упрощенным формулам FR1, FR2 и FR3, то метод перекрестного тестирования является предпочтительным, так как не требует приведения выражений формул к каноническому виду.

Заключение

Рассмотренные методы верификации вычислительных процессов с использованием покрытий и перекрестного тестирования являются алгоритмической основой построения САПР логических схем и программного продукта, в том числе и АУИСВ и Т.