Например, Бобцов

ГРАФО-АНАЛИТИЧЕСКИЕ МОДЕЛИ ВЫЧИСЛИТЕЛЬНЫХ ПРОЦЕССОВ В САПР

10

ГРАФО-АНАЛИТИЧЕСКИЕ МОДЕЛИ ВЫЧИСЛИТЕЛЬНЫХ ПРОЦЕССОВ В САПР
СИСТЕМЫ АВТОМАТИЗИРОВАННОГО ПРОЕКТИРОВАНИЯ

УДК 681.142.2
ГРАФО-АНАЛИТИЧЕСКИЕ МОДЕЛИ ВЫЧИСЛИТЕЛЬНЫХ ПРОЦЕССОВ В САПР
А.Г. Зыков, А.В. Безруков, О.Ф. Немолочнов, В.И. Поляков, А.В. Андронов
Рассматривается применение графо-аналитических моделей для верификации вычислительных процессов в рамках САПР, приводится пример построения комплексного кубического покрытия по графо-аналитической модели ациклического вычислительного процесса, формулируется задача синтеза тестовых наборов на основе кубического покрытия. Ключевые слова: графо-аналитические модели, верификация вычислительных процессов, кубические покрытия, тестирование.
Введение
Проблема анализа качества аппаратного и программного обеспечения становится сегодня все более острой, особенно по мере расширения использования информационных технологий и нанотехнологий в приборостроении. Экспоненциальный рост сложности аппаратного и программного обеспечения вычислительных процессов порождает повышенные требования к бездефектному проектированию. Известны примеры, как дорого обходятся ошибки, допущенные на различных этапах проектирования аппаратуры, поэтому все современные САПР обязательно снабжаются методологическими, программными и инструментальными средствами анализа разрабатываемого изделия на всех этапах автоматизированного проектирования. Не менее актуальными являются проблемы, связанные с обеспечением проектирования надежных программ. Однако возможности средств верификации сегодня заметно отстают от возможностей систем проектирования и технологии изготовления, поэтому разработка машинно-ориентированных методов верификации аппаратно-программных компонентов вычислительных процессов является актуальной [1]. Одним из направлений формализации верификации вычислительных процессов (ВВП) является использование их описания с помощью графо-аналитических моделей (ГАМ), на основании которого строится комплексное кубическое покрытие и синтезируются тестовые наборы [2].
Ставится задача нахождения допустимых значений переменных в системах неравенствотношений, определяющих условия-предикаты вычислительных процессов программ.
Построение комплексного покрытия ациклического вычислительного процесса
В работе [3] предложен метод верификации вычислительных процессов на основе алгебротопологического подхода. Рассмотрим работу метода на примере ГАМ простого интервального процесса (рис. 1).
Описание ГАМ можно готовить и редактировать в текстовом редакторе. В итоге получаем xmlописание ГАМ следующего вида (приведена часть описания):

Демонстрационная ГАМ для вычислительного процесса с множественным ветвлением



int 0 float

116

Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2011, № 4 (74)

А.Г. Зыков, А.В. Безруков, О.Ф. Немолочнов, В.И. Поляков, А.В. Андронов
0 1 In 4 2 x > 5 1 5 3 x > 0

In var: x
CV 1 x>5
F CV 2 x>0 F
CV 3 x 5 y = F2(x), x > 5
F3(x), x > 5

UV 7

3,4,5,6

Out var: y
Рис. 1. ГАМ вычислительного процесса для интервальной функции
Далее xml-описание ГАМ необходимо преобразовать в машинно-ориентированный вид. Для машинной обработки были разработаны специальные списочные структуры, представляющие ГАМ. Элементы этих структур изображены на рис. 2. После преобразования происходит поиск всех возможных кубов покрытия по алгоритму, представленному на рис. 3. Результат построения покрытия приведен в таблице (символ  обозначает произвольное значение из области определения предиката или переменной), где Y – предыдущее значение, а Y' – последующее значение переменной y.
На следующем этапе происходит определение значений входных переменных для того, чтобы процесс выполнялся по определенной ветви. Для этого, в общем случае, нужно найти хотя бы одно решение системы неравенств, задаваемой логическими выражениями в условных вершинах ГАМ. В общем виде такая система выглядит следующим образом:
F0 (a01, a02 , a03,...,a0i ) 
F1 (a11, a12 , a13,...,a1i ) ,
................................... Fk (ak1, ak 2 , ak3,...,aki )

Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2011, № 4 (74)

117

ГРАФО-АНАЛИТИЧЕСКИЕ МОДЕЛИ ВЫЧИСЛИТЕЛЬНЫХ ПРОЦЕССОВ В САПР
где Fk – логическое выражение для соответствующей условной вершины с номером k на проверяемой ветви, aki – значение переменной ai на этом этапе.
В рассматриваемой ГАМ для пути 1 – 4 – 7 (номера вершин) система примет вид
x  5 .
Для пути 1 – 2 – 5 – 7 получим x  0 x  5. Аналогично определяются системы отношений-неравенств и для остальных кубов покрытия.

Условная вершина:
Тип: CV
Имя или номер вершины

Входы zk
ADk

Переменные УП
r1, r2, …, ri AD1, AD2, …, ADi
FR УП

Выход zjT zjF
ADjT ADjF

Линейная вершина:
Тип: LV
Имя или номер вершины

Входы zk
ADk

Переменные УП r1, r2, …, ri
AD1, AD2, …, ADi

Выход zj
ADj

Объединяющая вершина:
Тип: UV
Имя или номер вершины

Входы z1, z2, …, zk
ADk

Выход zj
ADj

Рис. 2. Элементы списка машинного описания ГАМ

Start ГАМ

Выставить все CV в переход по True
CurNode = StartNode

Сохранить CurPath и состояние ГАМ в Result

GAM содержит CurNode T
CurNode уже посещалась

F T

Стек CV пуст

T

F CurNode = Стек CV.Pop()
CurPath = Paths.Pop() CurNode в переход по False

F FT
CurNode - CV

Result

Добавить CurNode в CurPath CurNode = CurNode.GetNext()

Добавить CurNode в стек CV Добавить CurPath в стек Paths

Finish

CV1 0 0 0 1
118

Рис. 3. Алгоритм построения кубического покрытия ГАМ

CV2 CV3 00 01 1 

Y    

Таблица. Кубическое покрытие ГАМ рис. 1

Y’  F3(x) F2(x) F1(x)

Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2011, № 4 (74)

А.Г. Зыков, А.В. Безруков, О.Ф. Немолочнов, В.И. Поляков, А.В. Андронов
Для определения значений переменных, участвующих в условных выражениях, сформулируем следующие правила. 1. Достаточно найти только одно решение для совокупности переменных условия-предиката, нет
необходимости решать систему со всей математической строгостью. 2. Не все переменные будут участвовать в каждом выражении, а многие будут участвовать в виде
константы, что упрощает решение системы. 3. Во многих случаях систему можно будет разделить на части, так как нередко вершины не связаны по
данным. 4. Часть ветвей программы будут в принципе недостижимы ни при каких ситуациях (don’t care),
некоторые из этих случаев можно определять без решения системы в целом. На последнем этапе с помощью синтезированных тестов проводится тестирование программного
обеспечения (ПО), на основании которого делается вывод о соответствии или несоответствии программы и ее спецификации.
Для реализации и исследования предложенного метода синтеза контролирующих тестов и дальнейших научно-исследовательских работ в области верификации вычислительных процессов разработана исследовательская САПР верификации вычислительных процессов (ИСАПР ВВП).
Общая структура исследовательской САПР ВВП
Итерационно-рекурсивная модель вычислительного процесса программ, предложенная в [4], является теоретической основой для разработки такой САПР, а в работе [5] сформулированы основные цели, которые преследуются при ее создании. С учетом этих положений предлагается следующая структура ИСАПР (рис. 4).
Ядро системы представляет собой набор системных и пользовательских плагинов, взаимодействующих друг с другом через единый интерфейс. Взаимодействие с хранилищем ведется через отдельный (общий для САПР) интерфейс, что позволяет унифицировать способ хранения и доступа к данным и применить любую доступную систему управления базами данных. Система для выполнения своей учебной функции также должна предоставлять три типа пользовательских интерфейса.

Рис. 4. Структурная схема ИСАПР ВВП
Под внешними интерфейсами подразумеваются способы обмена данными с информационными системами университета для более полной интеграции ИСАПР в учебный процесс.
Система разрабатывается как достаточно универсальная учебно-исследовательская среда, без привязки к определенному типу задач, но, так как в рамках работы рассматривается применение графоаналитических моделей для верификации ПО, то к реализации предлагается следующая схема взаимодействия модулей (рис. 5).

Рис. 5. Модули учебно-исследовательской САПР верификации на основе ГАМ
Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2011, № 4 (74)

119

ГРАФО-АНАЛИТИЧЕСКИЕ МОДЕЛИ ВЫЧИСЛИТЕЛЬНЫХ ПРОЦЕССОВ В САПР

Данное разделение на модули, очевидно, вытекает из схемы применения метода, представленной в [2]. Назначение модулей системы верификации следующее:  модуль «Анализатор кода» восстанавливает ГАМ на основе скомпилированной программы;  модуль «Редактор ГАМ» позволяет строить модели вручную на основе спецификации программы;  модуль «Структурирование ГАМ» упрощает полученные модели, выделяя в машинном
представлении ГАМ структурные единицы (что особенно важно для моделей, полученных от анализатора) [6];  назначение модулей «Вычисление покрытий ГАМ» [7] и «Синтез тестов» очевидно из их названий;  модуль «Тестировщик» создает необходимое для тестирования окружение и выводит результаты тестирования.
«Редактор ГАМ» работает только при непосредственном участии пользователя, остальные модули могут использоваться как в автоматическом, так и полуавтоматическом режиме.
Заключение
Использование предложенной схемы верификации на основе графо-аналитических моделей позволяет наглядно (на уровне логической структуры и, как следствие, интерфейса) продемонстрировать весь процесс верификации, а предложенная структура определяет проектирование и разработку исследовательской САПР верификации вычислительных процессов, позволяет сделать разработку отдельных модулей во многом независимой.
Литература
1. Bruce Wile, John C. Goss. Wolfgang Roesner. Comprehensive Functional Verification: The Complete Indastry Cycle. – San Francisco, 2005. – 676 c.
2. Зыков А.Г., Немолочнов О.Ф., Поляков В.И., Безруков А.В., Кузьмин В.В. Графо-аналитические модели как средство верификации вычислительных процессов // Труды Международного конгресса по интеллектуальным системам и информационным технологиям. Научное издание в 4-х томах. – М.: Физматлит, 2010. – Т. 2. – 400 с.
3. Немолочнов О.Ф., Зыков А.Г., Лаздин А.В., Поляков В.И. Верификация в исследовательских, учебных и промышленных системах // Научно-технический вестник СПб ГИТМО (ТУ). – 2003. – Вып. 11. – С. 146–151.
4. Немолочнов О.Ф., Зыков А.Г., Поляков В.И., Осовецкий Л.Г., Сидоров А.В., Кулагин В.С. Итерационно-рекурсивная модель вычислительных процессов программ // Изв. вузов. Приборостроение. – 2005. – Т. 48. – № 12. – С. 14–20.
5. Немолочнов О.Ф., Зыков А.Г., Поляков В.И., Петров К.В. Учебно-исследовательская САПР верификации и тестирования вычислительных процессов программ // Научно-технический вестник СПбГУ ИТМО. – 2006. – Вып. 32. – С. 127–128.
6. Немолочнов О.Ф., Зыков А.Г., Поляков В.И., Сидоров А.В. Структурирование программ и вычислительных процессов на множество линейных и условных вершин // Научно-технический вестник СПбГУ ИТМО. – 2005. – Вып. 19. – C. 207–212.
7. Немолочнов О.Ф., Зыков А.Г., Поляков В.И. Кубические покрытия логических условий вычислительных процессов и программ // Научно-технический вестник СПбГУ ИТМО. – 2004. – Вып. 14.– С. 225–233.

Зыков Анатолий Геннадьевич Безруков Александр Владимирович Немолочнов Олег Фомич Поляков Владимир Иванович Андронов Алексей Викторович

– Санкт-Петербургский государственный университет информационных технологий, механики и оптики, кандидат технических наук, доцент,
zykov_a_g@mail.ru – Санкт-Петербургский государственный университет информационных
технологий, механики и оптики, аспирант, versus1945@list.ru – Санкт-Петербургский государственный университет информационных
технологий, механики и оптики, доктор технических наук, профессор, зав. кафедрой, nemolochnov_o_f@mail.ru – Санкт-Петербургский государственный университет информационных технологий, механики и оптики, кандидат технических наук, доцент,
v_i_polyakov@mail.ru – Санкт-Петербургский государственный университет информационных
технологий, механики и оптики, аспирант, starsabre@mail.ru

120

Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики, 2011, № 4 (74)