автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.12, диссертация на тему:Методы верификации аппаратно-программных компонентов вычислительных систем

На правах рукописи □0345Т4(1

Зыков Анатолий Геннадьевич

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

Специальность - 05.13.12 "Системы автоматизации проектирования" (приборостроение)

АВТОРЕФЕРАТ диссертации на соискание учёной степени кандидата технических наук

1 2 ДЕК 2000

Санкт-Петербург 2008

003457471

Работа выполнена в Санкт-Петербургском государственном университете информационных технологий, механики и оптики

Научный руководитель

Защита диссертации состоится 23 декабря 2008г. в 15-50 часов в ауд. 466 на заседании диссертационного совета Д 212.227.05 при Санкт-Петербургском государственном университете информационных технологий, механики и оптики по адресу: 197101, г. Санкт-Петербург, Кронверкский пр., д. 49.

С диссертацией можно ознакомиться в библиотеке СПб ГУ ИТМО Автореферат разослан 21 ноября 2008 г.

профессор, доктор технических наук

О.Ф. Немолочнов

Официальные оппоненты: профессор, доктор технических наук доцент, кандидат технических наук

В.И. Анисимов В.Б. Тарасов

Ведущее предприятие

ФГУП ОКБ «Электроавтоматика» Санкт-Петербург

Учёный секретарь совета по защите докторских и кандидатских диссертаций Д 212.227.05

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность проблемы. Проблема анализа качества аппаратного и программного обеспечения становится сегодня все более острой, особенно по мере расширения использования нанотехнологий в приборостроении и информационных технологий при разработке программного обеспечения. Экспоненциальный рост сложности аппаратного и программного обеспечения вычислительных процессов порождает повышенные требования к бездефектному проектированию. Известны примеры, как дорого обходятся ошибки, допущенные на различных этапах проектирования, поэтому все современные САПР обязательно снабжаются методологическими, программными и инструментальными средствами анализа разрабатываемого изделия на всех этапах автоматизированного проектирования. Не менее актуальными являются проблемы, связанные с обеспечением проектирования надежных программ. Большой вклад в становление и развитие методов решения данной проблемы внесли отечественные ученые Пархоменко П.П., Липаев В.В., Согомонян Е.С., Майоров С.А., Немолочнов О.Ф., Рябов Г.Г., Селютин В.А., Курейчик В.М. и многие другие.

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

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

• разработать универсальную модель последовательностной схемы;

• разработать модель вычислительного процесса;

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

• разработать методы верификации аппаратно-программных компонентов вычислительных систем;

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

Научная новизна. В работе получены следующие существенные результаты:

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

• разработана концептуальная итерационно-рекурсивная двухконтур-ная модель вычислительного процесса;

• разработан метод построения комплексного кубического покрытия цифровой схемы;

• разработан метод построения комплексного кубического покрытия графо-аналитической модели (ГАМ) программы;

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

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

Внедрение результатов. Разработанная УИ САПР верификации и тестирования вычислительных процессов используется в СПб ГУ ИТМО на кафедре информатики и прикладной математики для анализа результатов лабораторных работ по курсам «Верификация моделей», «Системное программное обеспечение», «Программирование на языке ассемблер», «Технология программирования» для студентов специальности 220100 «Вычислительные машины, системы, комплексы и сети» и по курсу «Автоматизация логического проектирования ЭВС» для студентов специальности 210202 «Проектирование и технология вычислительных средств».

Результаты работы были использованы при выполнении проекта «Рефрен - Н» в ФГУП СПб ОКБ «Электроавтоматика», а также в ФГУП «Научно-исследовательский институт физической оптики, оптики лазеров и информационных оптических систем» Всероссийского научного центра «Государственный оптический институт им. С.И. Вавилова».

Апробация работы: Основные результаты диссертационной работы докладывались и получили одобрение на научных и учебно-методических конференциях профессорско-преподавательского состава ГИТМО(ТУ) (С.-Петербург 1996 - 2000, 2002, 2003 г.г.) и СПб ГУ ИТМО (С.-Петербург 2004 - 2008 г.г.); на Межвуз. науч. -техн. семинаре с междунар. участием «Автоматизация проектирования, технология элементов и узлов компьютерных систем». - СПб: 1998; на Всероссийской НТК «Интеллектуальные САПР-94», Таганрог, 1994; на Юбилейной НТК ППС, посвященная 100-летию университета 29-31 марта 2000 года.- СПб.: СПб ГИТМО (ТУ), 2000; на 6-й МНПК «Безопасность и защита информации сетевых техноло-

гий. COMMON CRITERIA" СПб, 13-15 нюня 2001.- СПб.: СПб ГИТМО (ТУ), 2001; на 9-й научно-технической конференции «Теория и технология программирования и защиты информации, применение вычислительной техники» -СПб: СПбГУ ИТМО 2002г.; на Международных научно-технических конференциях «Интеллектуальные системы» (IEEE AIS'04) и «Интеллектуальные САПР» (CAD-2002, 2004 - 2008) Дивноморское; на 11-ой международной научно-практической конференции «Теория и технология программирования и защиты информации»/ СПб: СПбГУ ИТМО, 18 мая 2007; на Первом СПб конгрессе «Профессиональное образование, наука, инновации в XXI веке» / СПб: СПбГУ ИТМО, 26-27 октября 2007.

Публикации. По материалам диссертации опубликовано 36 работ, в том числе - 12 из списка, рекомендованного ВАК.

Структура и объем работы Диссертация состоит из введения, четырех глав, заключения, библиографического списка из 92 наименований, содержит 105 страниц текста, 44 рисунка и 5 таблиц.

СОДЕРЖАНИЕ РАБОТЫ

Во введении обоснована актуальность темы, определены цели и методы исследования.

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

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

При анализе аппаратных компонентов выделяют такие методы, как моделирование, верификацию и тестирование. Моделирование и формальная верификация являются основными методами функциональной верификации.

Отмечено, что в таких САПР, как Cadence, Mentor Graphic, Synopsis, Polis и др. основной анализ проводится с помощью подсистем моделирования с использованием FSM - моделей.

При анализе ПО выделяют два основных метода контроля и анализа программ: статический и динамический. Статические методы основаны на исследовании тех или иных свойств ПО без его выполнения с использова-

нием различных инструментальных сред. Наиболее широкое распространение имеют следующие методы статического контроля:

• синтаксический контроль;

• контроль структурированности ПО;

• контроль правдоподобия программ;

• верификация ПО.

Методы верификации основаны на доказательстве корректности или некорректности ПО, соответствии разработанного ПО его спецификациям. Верификация ПО весьма сложна, но практически гарантирует правильность полученного ПО относительно сформулированных для него спецификаций. К недостаткам методов верификации можно отнести то, что формирование метаописания ПО весьма сложно. Кроме того, верификация практически не применяется на поздних этапах жизненного цикла ПО.

Существует два основных вида тестирования ПО:

• функциональное тестирование;

• структурное тестирование.

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

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

Во второй главе предложена универсальная модель последователь-ностной схемы. В общем виде любое цифровое устройство может быть представлено в виде операционного устройства (ОУ) и устройства управления (УУ). Устройство управления в отличии от ОУ имеет, как правило, нерегулярную структуру и задача построения его моделей является сложной проблемой и актуальна при проектировании микропроцессоров, заказных БИС, устройств на базе ПЛИС и т.п.. Методы построения моделей УУ в виде графа структурно-временного автомата достаточно исследованы и в работе не рассматриваются. В качестве модели функционально-логической схемы УУ в самом общем виде предлагается модель, представленная на рис. 1. Здесь вектор А' есть независимые входы схемы, из которых особо выделены сигнал синхронизации Т и сигнал начальной установки элементов памяти Л, который может быть как асинхронным сбросом, так и синхронизированным тактом Т, что в общем случае не является принципиальным. Значение сигналов обратной связи У разбито на два подмножества У*' и У?,

соответственно }" = Значения У' определены как булевы функ-

ции }" = }"(Л',)'). Значения выходных сигналов также определены как 7. = 2( Х,У) для автомата Мили и как 2 = 7.(Г) для автомата Мура. Для схемы также определены некоторые промежуточные сигналы ¿/¡, как выходы комбинационных подсхем (КС), которые являются вспомогательными и введены как следствие разбиения КС на одновыходные комбинационные подсхемы. Значение вектора сигналов У определяет предыдущее значение состояния схемы, а значение вектора }" - последующее состояние. В общем случае векторы У и У' задают некоторые классы состояний. Любой сигнал у и у' может принимать три значения: 0,1 и х, где х - есть безразличное состояние, которое произвольным образом можно доопределить в значение 1 или 0, если это не вызывает противоречия при переходе схемы из состояния У в состояние У

1= 2(Х, И

^ ^ г= Г(.у, П

| Г.5

Рис. 1. Универсальная модель функционально-логической схемы

Соответствие между значениями сигналов Г и У' определяется по интервальным покрытиям С( у') = С \ у') и С''(у'), где С'( у') есть область установки иС'(у') есть область хранения. Если некоторое значение у' вычислено кубом с е С г( у'), то у=х и у '=р, если же значение у' вычислено кубом С е Ср(у'), то значение у = у' = р.

В соответствии с предложенной структурной моделью схемы (рис. 1) введено понятие куба единого формата Фо = X )'и }А '¿к УЛ1)'л 2 Данный формат в векторном виде описывает все значения сигналов и их разбиение

на функциональные классы. Если не делать различия между классами У", У5, У'м и У*5, то можно ограничиться форматом Ф1 = ХУ 2ц У 2. Далее, если Хк отсутствуют, можно ограничиться форматом Ф2 = X У У 2 и, наконец, для случая, когда рассматриваются только переходы схемы, можно перейти к формату Ф, = X У У', что является вполне допустимым при теоретическом рассмотрении состояний и переходов схемы, так как значения 2ц и 2 являются импликациями от независимых входов X и сигналов обратной связи У или У' и их можно вычислить после построения переходов.

При построение графа переходов схемы возможен поиск переходов схемы в прямом или обратном направлении. Любой переход схемы может быть представлен в виде вектора: А'У У. Здесь значение вектора У является исходным состоянием схемы, а У' - последующим состоянием, в которое схема переходит под действием входных сигналов Хв исходном состоянии схемы. Так как УУ является сильно связанным устройством, можно ограничиться построением графа переходов в прямом направлении. В этом случае необходимо отдельно рассмотреть вопрос о поиске начальной вершины графа переходов схемы, а именно, переход из безразличного состояния сигналов обратной связи У = (хх...х) в некоторое множество исходных состояний У. Поиск таких переходов можно осуществить путем пересечения покрытий { С( у' ) } между собой при условии наложения ограничений на значение сигналов обратной связи У. При поиске начальных вершин:

V = Г)с,(у') , при У = хх...х, и при поиске последующих вершин графа переходов:

У 1*1 = Пс,(/),приУ= У/.

Теперь по изоморфизму построенного графа переходов функционально-логической схемы УУ графу структурно-временного автомата можно сделать заключение, что рассматриваемые модели верифицированы.

В работе рассматривается алгебро-топологическая модель последо-вательностной схемы в виде комплексного кубического покрытия. Для САПР одним из наиболее компактных и информационных является описание схем в виде кубических покрытий. Предложенная выше универсальная модель последовательностной схемы является основой для построения комплексного покрытия схемы. При этом схема декомпозируется на одно-выходные подсхемы, каждая из которых описывается вырожденными покрытиями С(/,) в локальном формате Фл = {X, У, У', 2}, где Х- независимые входы, У- сигналы обратной связи, определяющие исходное состояние схемы, У- сигналы обратной связи, определяющие последующее состояние схемы и 2 - выходные или внутренние значения комбинационных элементов (подсхем) схемы. Так как значения 2 являются импликациями

от независимых входов А'и сигналов обратной связи У и Г, то можно перейти к локальному формату Фл, = { X, У, )"}.

Построение комплексного покрытия всей схемы позволяет получить полную модель схемы для решения требуемых задач анализа. Комплексное кубическое покрытие (КР) строится в глобальном формате Фкс = { X, Г, У, Z }. Любой куб комплексного покрытия к, е КР трактуется как некоторое состояние логической схемы. КР строится методом пересечения множеств кубов покрытий подсхем на основе полного перебора, то есть всех возможных сочетаний. Таким образом:

КР = ПС(Я - {а | а с Ъ\а,Ь е КР),

где и количество покрытий подсхем.

Простой куб кс, есть такой куб, в котором ни одну координату со значением р = 1 или О, нельзя заменить на * без нарушения импликации у', -

р, и =р,.

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

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

Концептуальная двухконтурная модель вычислительных процессов программ приведена на рис. 2.

Рис.2. 'Двухконтурная итерационно-рекурсивная модель вычислительного процесса

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

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

• данные на входе вычислительного процесса могут изменяться только после его окончания путем перехода от Tin в Tout, т.е. рассматриваются только детерминированные (как результат дискретизации по времени) процессы.

Контуры обратной связи по управлению описывают циклы в программах и, соответственно, циклические вычислительные процессы, поро-

ждаемые ими, в любой их композиции и с любым уровнем вложенносги друг в друга.

Программа представляется как устройство управления в виде сдвигового регистра с бегущей единицей. Наличие значения z(y)=I означает исполнение некоторой текущей команды или вершины, являющейся замкнутым подмножеством команд на графо — аналитической модели (ГАМ).

Под циклом понимается некоторое замкнутое множество команд программы, которое может исполнятся два и более раз и имеет команду возврата по Jump или if Jump к ранее пройденному адресу. Наличие обращений к процедурам не нарушает данное положение, т.к. любая процедура может быть втянута в тело цикла. На ГАМ циклам будет соответствовать любое множество вершин, охваченных одним и только одним контуром обратной связи (КУо.с.). Контуры обратной связи соответствуют адресам возврата на продолжение цикла в программах и могут быть построены в процессе структурирования программного кода. Для кодирования и обозначения КУо.с. выделены специальные переменные yeY из множества управляющих вычислительным процессом ZzdY.

Для линеаризации логических уравнений, описывающих циклический вычислительный процесс, в КУо.с. вносится фиктивная точка разрыва, а значение переменной управления контуром обратной связи до точки разрыва обозначается как у и после точки разрыва - как у.

Значения логических переменных у и у', описывающих КУо.с., должны удовлетворять следующим соотношениям:

y'(t)=f[y(t)] и y(t+At): = y(t), т.е. значение y'(t) есть некоторая булева функция /от предыдущего значения y(t), а присвоение нового значения у' переменной у происходит в момент времени t+Jt, где At есть переменная задержка, равная времени исполнения тела цикла, что полностью соответствует разрыву сигналов обратной связи в логических схемах, например, при построении покрытий триггеров.

На основании разработанной модели ВП предложены примитивы и их вырожденные покрытия вершин ГАМ (рис.3).

Здесь через 2 обозначены переменные, которые инициализируют заданную вершину, а через z\ z' т и z'F - переменные передачи управления к следующим вершинам. Итеративные формулы обозначены как IFR, а рекуррентные - как RFR. В покрытиях выделены интервалы хранения (2=0) и вычисления (z=/). Вершина I'D для простоты показана для объединения трех дуг (Di, D2, D3 - входные дуги и Д, - выходная дуга). Заметим, что формулы IFR и RFR носят произвольный характер. В покрытии UD отображен тот факт, что инициализация г/ может быть только по одной из дуг.

Zr а Z/r 7 'F z2 Zj Z2 Z} z4

1 1 1 0 1 0 0 1

1 0 0 1 0 1 0 1

0 X 0 0 0 0 1 1

0 0 0 0

а) б)

LV! r=IFR i Lr" r—RFR ■

m- I 1 nv

Zr r r' ¿2 Zl r r' Zl

1 X /IFR/ 1 1 Pr IRFRI 1

0 Pr Pr 0 0 Pr Pr 0

в)

Рис.3. Примитивы и покрытия типовых вершин ГАМ: а) условной вершины (CV); б) объединения дуг (UD)\ в) линейной вершины (LV); УП -условие-предикат; nv - номер вершины; р, - предыдущее значение переменной г; х - безразличное значение переменной.

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

Для моделей одного уровня абстракции предложен метод верификации с использованием комплексных покрытий на основании операций # и м кубов комплексного покрытия анализируемых схем. Рассмотрим применение условий необходимости и достаточности при верификации схемных реше-

ний методом моделирования. Пусть задана некоторая булева функция / своими покрытиями С'([), при/= 1, и С°(/) при /= 0, которые построены произвольным методом, например по картам Карно. Требуется верифицировать некоторое схемное решение для / в виде логической схемы N ( с внешним выходом ZN ), спроектированной, например, эвристическим способом в произвольном базисе с применением методов факторизации, декомпозиции или их сочетания.

Необходимым условием верификации является совпадение реакций схемы N =1 ^ = 0) для V с е С'Ц) (Усе С°(/)).

Достаточным условием верификации является совпадение реакции мыгЫ=0(2Ы=1) для V с еС°(/) (V сеС'(/)).

Таким образом необходимым и достаточным условиями верификации схемы N является совпадение реакции схемы ZN со значениями булевой функции / для всех кубов с е С'(/) и С0 (/). Комплексное покрытие КР = С'(/) и С0 (/) и есть метамодель схемы И,

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

Построим метамодель схемы для значений выхода равных 0 и 1, в виде комплексного покрытия КР = С°(2Ы) и С'( 2Ы ). В этом случае требуется установить соответствие между покрытиями С'( / ) и С" ( / ) и С"(2Ы ) и С'( 2Ы), которое может быть выполнено либо с использованием операции вычитания кубов покрытий (#), либо с помощью операции пересечения кубов покрытий (П). При использовании операции вычитания для верификации схемы N необходимо, чтобы С'( /) # С'( 2Ы) = 0, и достаточно, чтобы С'( Ш) # С!({) = 0. Аналогично для покрытий С°(/) и С?(2Ы ). Из этого следует, что при использовании операции вычитания достаточно иметь только один тип покрытий: либо единичное С'( / ) и С'( 2Щ, либо нулевое С (X) и С°(2М).

Применение алгебро-топологических операций вычитания и пересечения покрытий позволяет при сравнении множеств избежать точного соответствия элементов множеств между собой, поэтому С'( / ) # С'( 2Ы) и С'( 2Ы) # С'(/) не соответствуют аналогам (не топологическим) обычного вычитания множеств ( А \ В и В \ А).

Итак, применив операции вычитания ( # ) и пересечения ( П ) покрытий при верификации объектов получим четыре возможных отношения:

1. С](/)#С'(2М) = 0 и С'( 2Ы) # С]( /) = 0, или С'(/)Г\С(Ш)=0 и С"(/) П С'( 2М) = 0 - условия полной верификации.

2. С'(/)#С!(2Ы)*0 и С'( 2Ы) # С'(/) = 0, или С'(/) П С°(2Ы) *0 и С°([) П С'( 2Ы) = 0 - есть необходимое, но недостаточное условие верификации.

3. с'(Л # С'(Щ = 0 и С'(Щ # С'(/) * 0, или с'(/) п С°(гм) =0 и С°(/) п С'^ * 0 - есть достаточное, но не необходимое условие верификации.

4. С'(/)#С'(Щ*0 и С'(Щ#С'(/)*0, или С'(/)гл (?(2Я) и С"^ п С'(ИЫ) 0 - условия верификации отсутствуют.

Во 2-ом и 3-ем случаях можно говорить о верификации частично определенных функций (объектов) с использованием «размытых» множеств, иначе говоря, один объект «делает» больше, чем другой. Таким образом, из вышеизложенного следует, что полная верификация существует только при выполнении соотношений 1-го случая. Данное рассуждение проведено для случая одновыходной схемы N и исходного покрытия булевой функции /, которое является простейшим случаем метамодели высшего ранга. Аналогичные методы можно применить при верификации граф-схем алгоритмов, конечных автоматов (абстрактных и структурных), многовыходных последовательностных схем и программ.

ГАМ, = ГАМ, ГАМ, = ГАМ2

Рис.4. Общая схема процесса верификации вычислительных процессов

На рис. 4 один и тот же вычислительный процесс реализован двумя различными способами. На схеме показано, что на основании технических

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

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

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

Рассмотрим пример верификации ациклического процесса. Пусть задана некоторая интервальная формула:

реализующая вычисления некоторой переменной г по различным формулам: /-Ш, /7?2 и 1-1(3 произвольного вида в зависимости от двух булевых переменных, задающих некоторые условия-предикаты в виде неравенств: а: х<к.1 и Ь: х > к2.

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

ГАМ вычисления переменной г приведены на рис.5. На рис.5.а) показана функциональная декомпозиция булевой функции / = Да,Ь) с начальной вершиной условия-предиката а (ГАМ 1), а на рис.5.6) - с начальной вершиной Ь (ГАМ 2).

FR1, при jtsi,; г = . FR2, при к1<х<к2\ FR3, при х^к2,

( >73

CVJ

( 1

QUI J

аЪ 00 01 11 10

ГК2 ГЯЗ РШ га/

аЪ 00

01

11

10

¡■112 1-КЗ га/

а) б)

Рис.5. ГАМ вычисления интервальной формулы

Построим комплексные кубические покрытия С/(г) и С2(г) для вычисляемой переменной г по ГАМ 1 и ГАМ 2:

сф-Н

21 а Ъ г г' г/ М 21 а Ъ г г' г2'

1 X X /га// 1 С1 ( 1 X 1 X /газ/ 1

1 0 1 X /газ/ 1 1 0 0 X /га2/ 1

1 0 0 X /га2/ 1 с3 С 1 1 0 X /га// 1

0 X X р р 0 10 X X -р р 0

{с}

С;

с3

С4

По покрытиям С ¡(г) и С2(г) построим тесты Т,(г) и Т2(г) путем пересечения кубов из интервальных частей покрытий С ¡(г) и С2&), соответственно. Получим тесты:

Ш-

21 а Ь г г' г г'

1 Г 0 X /га// 1

1 0' 0 X /га2/ 1

1 0 Г X /газ/ 1

1 0 0' X /га2/ 1

Г 0 1 р /газ/ 1

0' 0 1 р р о

Примеч. /,/1~1 е с/С'.сз из С ¡(г)

а Ъ /• г' г2' (0

1 0 1' X /газ/ 1 '1

1 0 0' X /га2/ 1

1 Г 0 X /га// 1 ь

1 0' 0 X /га2/ 1 Л

Г 1 0 р /га// 1 Ь

0' 0 1 р р о п

Пргшеч /// Г/ е с у Г с з из С ¡(г)

Заметим, что для формул должны выполняться условия: /У7/?// ф /РКП ф /газ/ Ф р, т.е. вычисляемые и хранимые значения должны различаться на

разных наборах теста Штрихами в тестах отмечены значения активно изменяемых условий-предикатов.

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

Перекрестное тестирование дает следующий результат: К1(Т1)=Н2(Т,) и Я1(Т2)=Я2(Т2), что также подтверждает эквивалентность вычислительных процессов. Заметим, что если переменную г вычислять по разным упрощенным формулам РШ, РЯ2 и РИЗ, то метод перекрестного тестирования является предпочтительным, так как не требует приведения выражений формул к каноническому виду.

В четвертой главе диссертационной работы приводятся машинно-ориентированные алгоритмы реализации основных операций по вычислению комплексных кубических покрытий. Алгоритм построения комплексного кубического покрытия представлен на рис. 6.

Рис. 6. Алгоритм построения комплексного кубического покрытия На рис. 7. приводится структура учебно-исследовательской САПР верификации вычислительных процессов (УИ САПР ВВП)

База знаний База данных

Рис.7. Структурная схема экспериментальной САПР

Система представляет собой консольное приложение для ОС Windows NT/2000 /ХР и является программной реализацией разработанных в диссертационной работе алгоритмов. Дано описание состава модулей, входящих в систему. УИ САПР ВВП состоит из трех основных частей: базы знаний, базы данных и монитора управлениями событиями.

В заключении содержатся основные результаты, полученные в диссертационной работе.

1. Предложена универсальная модель последовательностной схемы. На основе предложенной модели разработана методика построения комплексного кубического покрытия схемы для различных задач анализа в САПР.

2. Разработана концептуальная итерационно-рекурсивная двухкон-турная модель вычислительного процесса.

3. Предложена модель вычислительного процесса в виде орграфа и кубических покрытий условий-предикатов для вычисляемых переменных.

4. Для машинно-ориентированного описания ГАМ предложены примитивы и вырожденные покрытия типовых вершин.

5. Предложены методы верификации через эквивалентность покрытий и перекрестное тестирование вычислительного процесса вне зависимости от его физической реализации.

6. Разработана методика структурирования вычислительного процесса путем разбиения множества команд машинного кода на замкнутые подмножества команд с одной точкой входа и одной точкой выхода.

7. Разработана структура экспериментальной учебно-исследовательской САПР верификации вычислительных процессов, алгоритмы и программы решения отдельных задач, в частности: построение комплексного покрытия схемы, построение графа и покрытий частично определённых булевых функций, моделирования логических неисправностей условий-предикатов.

Список работ, опубликованных по теме диссертации

1. Блохин В.Н., Голованевский Г.Л., Зыков А.Г., Немолочнов О.Ф. Доступная система контроля цифровых узлов и верификация логических модулей. / Сб. «ЭВМ в проектировании и производстве» / Вып. 4, «Машиностроение», 1989.

2. Зыков А.Г., Немолочнов О.Ф. Автоматная модель устройства управления в САПР при верификации проекта. / Межвузовский сборник научных трудов «Автоматизированное проектирование в радиоэлектронике и приборостроении», С.-Пб, ГЭТУ, 1994. С. 21-23.

3. Зыков А.Г., Немолочнов О.Ф. Создание моделей сложных процессоров при верификации проектов. / Материалы Всероссийской НТК «Интеллектуальные САПР-94», Таганрог, 1994.

4. Зыков А.Г. Построение моделей устройств управления микропроцессоров в виде абстрактного графа автомата. / Тезисы док. Межвуз. науч. -техн. семинара с междунар. участием «Автоматизация проектирования, технология элементов и узлов компьютерных систем». - СПб:

1998. С. 3-4

5. Зыков А.Г., Немолочнов О.Ф. К вопросу верификации функционально-логической схемы на основе абстрактного графа автомата. / Тезисы док. Межвуз. науч. -техн. семинара с междунар. участием «Автоматизация проектирования, технология элементов и узлов компьютерных систем». - СПб: 1998. С. 5-6.

6. Зыков А.Г., Копорский Н.С., Лаздин A.B. К вопросу о принципах верификации результатов имитационного моделирования комплек-сированных оптоэлектронных систем. / Тезисы док. Межвуз. НТС с междунар. участием «Автоматизация проектирования, технология элементов и узлов компьютерных систем». - СПб: 1998. С.6.

7. Зыков А.Г., Немолочнов О.Ф. Функционально-логическая модель устройства управления / Тезисы докладов XXX НТК ППС -СПб.: СПбГИТМО (ТУ), 1999. С. 90.

8. Немолочнов О.Ф., Зыков А.Г. Построение графа переходов устройства управления по функционально-логической схеме. / Тезисы докладов XXX НТК ППС СПбГИТМО (ТУ) - СПб.: СПб ГИТМО (ТУ),

1999. с. 95.

9. Немолочнов О.Ф., Поляков В.И., Зыков А.Г. Верификация и тестирование программ по проблеме 2000 года (смены дат). / Тезисы докладов. Часть II. Юбилейная НТК ППС, посвященная 100-летию университета 29-31 марта 2000 года,- СПб.: СПб ГИТМО (ТУ), 2000. с.З.

Ю.Зыков А.Г., Немолочнов О.Ф. Метод пересечения покрытий как средство анализа функционально-логических схем. / Тезисы докладов. Часть II. Юбилейная НТК ППС, посвященная 100-летию университета 29-31 марта 2000 года.- СПб.: СПб ГИТМО (ТУ), 2000. с.5.

11. Зыков А.Г., Немолочнов О.Ф. Метод пересечения покрытий с ограничением при решении задач верификации проекта. / Тезисы докладов. Часть II. Юбилейная НТК ППС, посвященная 100-летию университета 29-31 марта 2000 года,- СПб.: СПб ГИТМО (ТУ), 2000. с.6.

12.Воробьев A.B., Зыков А.Г., Поляков В.И., Шевченко A.A. Обеспечение безопасности функционирования распределенных информационно-управляющих систем. / Труды 6-й МНПК «Безопасность и защита информации сетевых технологий. COMMON CRITERIA" СПб, 13-15 июня 2001,- СПб.: СПб ГИТМО (ТУ), 2001. с.33-34.

13. Зыков А.Г., Немолочнов О.Ф., Поляков В.И. Формализация ограничений на пересечение множеств кубов при верификации. / Известия ТРТУ. №3 (26) Тематический выпуск «Интеллектуальные САПР». Материалы Международной НТК «Интеллектуальные САПР». -Таганрог: Изд-во ТРТУ, 2002. с. 198-199.

14. Зыков А.Г., Немолочнов О.Ф., Поляков В.И. Универсальная модель последовательностных схем в САПР / Научно-технический вестник СПБ ГИТМО (ТУ). Выпуск 6. Информационные, вычислительные и управляющие системы / Гл. ред. В.Н. Васильев.- СПб.: СПб ГИТМО (ТУ), 2002. с. 107-108.

15. Зыков А.Г., Немолочнов О.Ф., Поляков В.И. Построение комплексного покрытия последовательностных схем методом пересечения покрытий систем булевых функций / Научно-технический вестник СПБ ГИТМО (ТУ). Выпуск 6. Информационные, вычислительные и управляющие системы / Гл. ред. В.Н. Васильев.- СПб.: СПб ГИТМО (ТУ), 2002. с.109-111.

16. Зыков А.Г., Немолочнов О.Ф., Поляков В.И. Верификация моделей цифровых устройств в САПР. / Труды Международных конференций «Искусственные интеллектуальные системы»(1ЕЕЕ AIS'02) и «Интеллектуальные САПР» (CAD-2002). Научное издание. - М.: Издательство Физматлит, 2002. -609 с. -ISBN 5-940520031-6/. С.320-323.

17. Зыков А.Г., Немолочнов О.Ф., Виноградов Ю.Н., Поляков В.И. Верификация как средство отладки моделей различного уровня. / «Известия вузов. Приборостроение»/ Том 46, №2, СПб, февраль 2003. с.51-55.

18. Немолочнов О.Ф., Зыков А.Г., Лаздин A.B., Поляков В.И. Верификация в исследовательских, учебных и промышленных системах / Научно-технический вестник СПбГУ ИТМО. Выпуск 11. Актуальные проблемы анализа и синтеза сложных технических систем. / Под ред. В.О. Никифорова- СПб: СПбГУ ИТМО, 2003. С. 146-151.

19. Зыков А.Г., Немолочнов О.Ф., Поляков В.И. Методы верификации цифровых устройств / Труды Международных научно-технических конференций «Интеллектуальные системы» (IEEE A1S'04) и «Интеллектуальные САПР» (CAD-2004). Научное издание и 3-х томах. М.: Изд-во Физматлит, 2004, Т.2. - 468 с. -ISBN 5-9221-0531-5. С. 39-41.

20. Зыков А.Г., Немолочнов О.Ф., Поляков В.И. Методы и алгоритмы анализа цифровых устройств в САПР / Труды Международных научно-технических конференций «Интеллектуальные системы» (IEEE AIS'04) и «Интеллектуальные САПР» (CAD-2004). Научное издание и 3-х томах. М.: Изд-во Физматлит, 2004, Т.2. - 468 с. -ISBN 5-9221-05315. С. 41-45.

21. Немолочнов О.Ф., Зыков А.Г., Поляков В.И. Кубические покрытия логических условий вычислительных процессов и программ. / Научно-технический вестник СПбГУ ИТМО. Выпуск 14. Информационные технологии, вычислительные и управляющие системы. / Гл. ред. В.Н. Васильев.- СПб: СПбГУ ИТМО, 2004. с.225-233.

22. Немолочнов О.Ф., Зыков А.Г., Поляков В.И., Сидоров A.B. Структурирование программ и вычислительных процессов на множество линейных и условных вершин / Научно-технический вестник СПбГУ ИТМО. Выпуск 19. Программирование, управление и информационные технологии / Гл. ред. В.Н. Васильев,- СПб: СПбГУ ИТМО, 2005. с.207-212.

23. Немолочнов О.Ф., Зыков А.Г., Поляков В.И., Осовецкий Л.Г., Сидоров A.B., Кулагин B.C. Итерационно-рекурсивная модель вычислительных процессов программ / «Известия вузов. Приборостроение» / Том 48, №12, СПб, декабрь 2005, С.14-20.

24. Немолочнов О.Ф., Зыков А.Г., Поляков В.И. Методы анализа вычислительных процессов программ в исследовательских и учебных проектах / Труды межд.конф. «Интеллектуальные системы» (AIS'05) и «Интеллектуальные САПР» (CAD-2005), Научное издание в 3-х томах-М.: Физматлит, 2005,Т2.532с,- ISBN 5-9221-0621-Х. С.424-430.

25. Немолочнов О.Ф., Зыков А.Г., Поляков В.И., Кулагин B.C., Петров К.В. Логические неисправности вычислительных процессов программ / Труды 9-й научно-технической конференции «Теория и технология программирования и защиты информации, применение вычислительной техники» -СПб: СПбГУ ИТМО, 18 мая 2005. С.2-3.

26. Комплексные кубические покрытия и графо-аналитические модели как средство описания вычислительных процессов программ /

Немолочнов О.Ф., Зыков А.Г., Поляков В.И. /Труды Международных научно-технических конференций «Интеллектуальные системы» (AIS'06) и «Интеллектуальные САПР» (CAD-2006), Научное издание в 3-х томах-М.: Физматлит, 2006, Т2.- 588с. - ISBN 5-9221-0686-4. С.3-7.

27. Моделирование простых логических неисправностей вычислительных процессов программ / Немолочнов О.Ф., Зыков А.Г., Поляков

B.И., Петров К.В. / Научно-технический вестник СПбГУ ИТМО. Выпуск 32. Информационные технологии: теория, методы, приложения / Гл. ред. В.Н. Васильев,- СПб: СПбГУ ИТМО, май 2006. С. 113-118.

28. Учебно-исследовательская САПР верификации и тестирования вычислительных процессов программ / Немолочнов О.Ф., Зыков А.Г., Поляков В.И., Петров К.В. / Научно-технический вестник СПбГУ ИТ-МО. Вып>ск 32. Информационные технологии: Теория, методы, приложения / Гл. ред. В.Н. Васильев,- СПб: СПбГУ ИТМО, май 2006. С. 127128.

29. Методы тестирования вычислительных процессов /Немолочнов О.Ф., Зыков А.Г., Осовецкий Л.Г., Поляков В.И. / Научно-технический вестник СПбГУ ИТМО. Выпуск 45. Информационные технологии: теория, методы, приложения / Гл. ред. В.Н. Васильев,- СПб: СПбГУ ИТМО, май 2007. С.121-125.

30. Методы формализации графо-аналитических моделей вычислительных процессов программ / Немолочнов О.Ф., Зыков А.Г., Поляков В.И. / Труды Международных научно-технических конференций «Интеллектуальные системы» (AIS'07) и «Интеллектуальные САПР» (CAD-2007), Научное издание в 4-х томах-М.: Физматлит, 2007, Т.З.-496с. - ISBN 978-5-9221-0856-0. С.88-96.

31. Модель и примитивы покрытий вершин циклических вычислительных процессов / Немолочнов О.Ф., Зыков А.Г., Осовецкий Л.Г., Поляков В.И. //Известия вузов. Приборостроение. 2007. Том 50, №8,

C.18-23.

32. Структурирование вычислительного процесса по программному коду / Немолочнов О.Ф., Зыков А.Г., Осовецкий Л.Г., Поляков В.И. // - Труды 11 -й международной научно-практической конференции «Теория и технология программирования и защиты информации»/ СПб: СПбГУ ИТМО, 18 мая 2007. С.7-9.

33. Автоматизированная учебно-исследовательская система верификации и тестирования программ / Немолочнов О.Ф., Зыков А.Г., Осовецкий Л.Г., Петров К.В. // Труды Первого Санкт-Петербургского конгресса «Профессиональное образование, наука, инновации в XXI веке» / СПб: СПбГУ ИТМО, 26-27 октября 2007. С.209-210.

34. Верификация как средство бездефектного проектирования программных продуктов / Немолочнов О.Ф., Зыков А.Г., Осовецкий Л.Г. // Труды Первого Санкт-Петербургского конгресса «Профессиональное

образование, наука, инновации в XXI веке» / СПб: СПбГУ ИТМО, 26-27 октября 2007. С.221-223.

35. Тестирование логических неисправностей вычислительных процессов в программах / Немолочнов О.Ф., Зыков А.Г., Осовецкий Л.Г., Поляков В.И., Петров К.В. / Журнал «Информационные технологии»/№12, М., 2007, С.2-5.

36. Импликация и неопределенные значения условий-предикатов вычислительных процессов / Немолочнов О.Ф., Зыков А.Г., Поляков В.И. / Труды Международных научно-технических конференций «Интеллектуальные системы» (AIS'08) и «Интеллектуальные САПР» (CAD-2008), Научное издание в 4-х томах. - М.: Физматлит, 2008, Т.1.- 400с. -ISBN 978-5-9221-0922-2. С. 140-145.

Тиражирование и брошюровка выполнены в учреждении «Университетские телекоммуникации» 197101, Санкт-Петербург, Саблинская ул., 14 Тел. (812) 233 4669 объем 1,0 п.л. Тираж 100 экз.

Введение.

Глава 1. Обзор методов верификации аппаратных и программных компонентов вычислительных систем.

1.1 Основные термины и определения.

1.2 Место верификации при проектировании вычислительных систем.

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

1.3.1. Методы верификации на основе темпоральных логик.

1.3.2. Методы на базе автоматных и графовых моделей.

1.3.3. Алгебраические методы.

1.3.4 Методы'верификации программ.

1.4 Современные тенденции в методологии верификации аппаратных и программных компонентов ВС.

1.5 Вычислительные процессы в логических схемах и программах.

1.5.1. Проектирование вычислительных процессов.

1.5.2. Вычислительный процесс.

1.5.3 Верификация вычислительных процессов.

1.6 Постановка задач исследования.

Выводы по главе 1.

Глава 2. Разработка моделей вычислительного процесса.

2.1 Разработка универсальной модели функционально-логической схемы.

2.2 Алгебро-топологическая модель последовательностной схемы в виде комплексного кубического покрытия.

2.3 Итерационно-рекурсивная модель вычислительных процессов в виде комплексных кубических покрытий.

2.3.1 Структурирование программ и вычислительных процессов.

2.3.2 Концептуальная итерационно-рекурсивная модель (ШМО).

2.3.3 Итерационно-рекурсивные покрытия.

2.4 Модель и примитивы вершин циклических вычислительных процессов.

2.4.1 Итерационно-рекурсивная модель вычислительного процесса. с двумя контурами обратной связи.

2.4.2 Примитивы вырожденных покрытий вершин ГАМ.

2.4.3 Построение комплексного покрытия для циклических. вычислительных процессов.

2.4.4 Машинно-ориентированное описание вершин и дуг ГАМ.

Выводы по главе 2.

Глава 3. Разработка методов верификации вычислительных процессов.

3.1 Верификации моделей разного уровня методом построения графа переходов схемы

3.2. Верификация моделей одного уровня абстракции.

3.2.1 Методы верификации цифровых схем.

3.3 Разработка методов верификации программ.

3.3.1 Метод функциональной верификации программ на основе. алгебро-топологического подхода.

3.3.2. Кубические покрытия логических условий вычислительных. процессов и программ.

3.4. Методы верификации вычислительных процессов.

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

Выводы по главе 3.

Глава 4. Разработка структуры и алгоритмов учебно-исследовательской САПР верификации вычислительных процессов.

4.1 Структура УИ САПР ВВП ФЛС. Базы знаний и данных при построении моделей

4.2 База Знаний и База данных УИ САПР ВВП ФЛС.

4.2.1 Структура, формирование и редактирование Базы Знаний.

4.2.2 Разработка алгоритмов взаимодействия БД и БЗ. Протокол. обмена данными.

4.3 Машинно-ориентированные алгоритмы реализации операций пересечения и поглощения кубов комплексного покрытия.

4.4 Входной язык описания схемы.

4.5 Разработка алгоритма построения моделей цифровых устройств в виде комплексного кубического покрытия.

4.6 Разработка алгоритмов верификации.

4.7 Обобщенная структура УИ САПР ВВП.

Выводы по главе 4.

Актуальность проблематики диссертационной работы

Проблема анализа качества аппаратного и программного обеспечения становится сегодня все более острой, особенно по мере расширения использования нанотехнологий в приборостроении и информационных технологий при разработке программного обеспечения. Экспоненциальный рост сложности аппаратного и программного обеспечения вычислительных процессов порождает повышенные требования к бездефектному проектированию. Известны примеры, как дорого обходятся ошибки, допущенные на различных этапах проектирования, поэтому все современные САПР обязательно снабжаются методологическими, программными и инструментальными средствами анализа разрабатываемого изделия на всех этапах автоматизированного проектирования. Не менее актуальными являются проблемы, связанные с обеспечением проектирования надежных программ. Большой вклад в становление и развитие методов решения данной проблемы внесли отечественные ученые Пархоменко П.П., Липаев В.В., Согомонян Е.С., Майоров С.А., Не-молочнов О.Ф., Рябов Г.Г., Селютин В.А., Курейчик В.М. и многие другие.

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

Цель работы является исследование и разработка методов верификации аппаратно-программных компонентов вычислительных систем; разработка машинно-ориентированных алгоритмов построения комплексных кубических покрытий цифровых схем и графо-аналитических моделей программ; разработка структуры и основных подсистем учебно-исследовательской САПР (УИ САПР) верификации вычислительных процессов.

Для достижения поставленной цели в работе решались следующие основные задачи:

• сравнительный анализ существующих методов верификации проектов;

• разработка универсальной модели последовательностной схемы;

• разработка модели вычислительного процесса;

• разработка методов и алгоритмов построения комплексных кубических покрытий цифровых схем и программ;

• разработка методов верификации аппаратно-программных компонентов вычислительных систем;

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

Научная новизна. В работе получены следующие существенные результаты:

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

• разработана концептуальная итерационно-рекурсивная двухконтурная модель вычислительного процесса;

• разработан метод построения комплексного кубического покрытия цифровой схемы;

• разработан метод построения комплексного кубического покрытия графо-аналитической модели (ГАМ) программы;

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

• на основе разработанных методов предложены алгоритмы работы учебно-исследовательской САПР верификации вычислительных процессов и отдельных подсистем.

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

Внедрение результатов работы. Основные результаты работы использованы в СПб ГУ ИТМО на кафедре информатики и прикладной математики в учебных дисциплинах «Верификация моделей», «Системное программное обеспечение», «Технология программирования» для студентов специальности 220100 «Вычислительные машины, системы, комплексы и сети» и по курсу «Автоматизация логического проектирования ЭВС» для студентов специальности 210202 «Проектирование и технология вычислительных средств».

Результаты работы были использованы при выполнении проекта «Рефрен - Н» в ФГУП СПб ОКБ «Электроавтоматика», а также в ФГУП «Научно-исследовательский институт физической оптики, оптики лазеров и информационных оптических систем» Всероссийского научного центра «Государственный оптический институт им. С.И. Вавилова».

Апробация работы: Основные результаты диссертационной работы докладывались и получили одобрение на научных и учебно-методических конференциях профессорско-преподавательского состава ГИТМО(ТУ) (С.Петербург 1996 - 2000, 2002, 2003 г.г.) и СПб ГУ ИТМО (С.-Петербург 2004 -2008 г.г.); на Межвуз. науч. -техн. семинаре с междунар. участием «Автоматизация проектирования, технология элементов и узлов компьютерных систем». - СПб: 1998; на Всероссийской НТК «Интеллектуальные САПР-94», Таганрог, 1994; на Юбилейной НТК 1111С, посвященная 100-летию университета 29-31 марта 2000 года.- СПб.: СПб ГИТМО (ТУ), 2000; на 6-й МНПК «Безопасность и защита информации сетевых технологий. COMMON CRITERIA" СПб, 13-15 июня 2001.- СПб.: СПб ГИТМО (ТУ), 2001; на 9-й научно-технической конференции «Теория и технология программирования и защиты информации, применение вычислительной техники» -СПб: СПбГУ ИТМО 2002г.; на Международных научно-технических конференциях «Интеллектуальные системы» (IEEE AIS'04) и «Интеллектуальные САПР» (CAD-2002, 2004 - 2008) Дивноморское; на 11-ой международной научно-практической конференции «Теория и технология программирования и защиты информации»/ СПб: СПбГУ ИТМО, 18 мая 2007; на Первом СПб конгрессе «Профессиональное образование, наука, инновации в XXI веке» / СПб: СПбГУ ИТМО, 26-27 октября 2007.

Публикации. По материалам диссертации опубликовано 36 работ, в том числе - 12 из списка, рекомендованного ВАК.

Структура и объем работы Диссертация состоит из введения, четырех глав, заключения, библиографического списка из 92 наименований, содержит 105 страниц текста, 44 рисунка и 5 таблиц.

Выводы по главе 4

1. Разработаны машинно-ориентированные методы реализации основных операций построения комплексных кубических покрытий ФЛС.

2. Разработаны методы, алгоритмы и программы верификации аппаратно-программных компонентов вычислительных систем.

3. На основе предложенных методов разработана структура, основные алгоритмы и программы учебно-исследовательской САПР верификации вычислительных процессов.

4. Намечены пути дальнейших исследований в области верификации аппаратно-программных компонентов ВС.

Заключение

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

1. Предложена универсальная модель последовательностной схемы. На основе предложенной модели разработана методика построения комплексного кубического покрытия схемы для различных задач анализа в САПР.

2. Разработана концептуальная итерационно-рекурсивная двухкон-турная модель вычислительного процесса.

3. Предложена модель вычислительного процесса в виде орграфа и кубических покрытий условий-предикатов для вычисляемых переменных.

4. Для машинно-ориентированного описания ГАМ предложены примитивы и вырожденные покрытия типовых вершин.

5. Предложены методы верификации через эквивалентность покрытий и перекрестное тестирование вычислительного процесса вне зависимости от его физической реализации.

6. Разработана методика структурирования вычислительного процесса путем разбиения множества команд машинного кода на замкнутые подмножества команд с одной точкой входа и одной точкой выхода.

7. Разработана структура экспериментальной учебно-исследовательской САПР верификации вычислительных процессов, алгоритмы и программы решения основных задач, в частности: построение комплексного покрытия схемы, построение графа и покрытий частично определённых булевых функций, моделирования логических неисправностей условий-предикатов, верификации аппаратно-программных компонентов вычислительных систем.

1. Системы автоматизированного проектирования: Иллюстрированный словарь / Под ред. И.П. Норенкова. М.: Высшая школа, 1986.

2. CMMI for Systems Engineering/Software Engineering, Version 1.02 (CMMI-SE/SW, VI.02) CMU/SEI-2000-TR-018 ESC-TR-2000-018 November 2000, P. 598

3. Липаев B.B. Обеспечение качества программных средств. Методы и стандарты / Издательство: Синтер; Серия: Информационные технологии, 380 стр., 2001 г.

4. C.B. Зеленов, Н.В. Пакулин. Верификация компиляторов систематический подход/ Труды Института системного программирования РАН.

5. Г. Майерс. Надежность программного обеспечения. М.: «Мир», 1980. 360 с.

6. Грушин А.И. Верификация в вычислительной технике. //Потенциал, №4,2007: hltp://potcntia1.org.ru/Info/ArtDl200704151927РНЗ C4J4

7. M. Blum, H. Wasserman / Reflections on the Pentium Division Bug. IEEE Trans. On Computers, vol. 45, no. 1996, 4, April

8. Синицын C.B., Налютин Н.Ю. Верификация программного обеспечения // БИНОМ. Лаборатория знаний, Интернет-университет информационных технологий ИНТУИТ.ру, 2008

9. А.Лохов. Функциональная верификация СБИС в свете решений Mentor Graphics//3JIEKTP0HHKA: Наука, Технология, Бизнес Выпуск № 1/2004 С.58-62.10. 2001 Dataquest Sub-Market Analysis On Combined Verification Technologies. www.dalaquesi.com.

10. Дейкстра Э. Дисциплина программирования: Пер. с англ.- М.: Мир, 1978. -275с.

11. Грис Д. Наука программирования: Пер. с англ.- М.: Мир, 1984.416с.

12. Манна 3. Правильность программ // Кибернетический сборник. Новая серия. М., 1970.- Вып.7.-С.85-93.

13. Непомнящий В.А. Практические методы верификации программ // Кибернетика. 1984.- №2,- С.21-28, 43.

14. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. — М.: Радио и связь, 1988.- 256с.

15. Bakker J.W. Mathematical Theory of Program Correctness.- London: Prentice-ITall, 1980,- 505c.

16. Clarke E., Mishra B. Automatic Verification of Asyncronous Circuits // Logic of Programs. Proc. 1983 / E. Clarke and D.Kozen (eds.). Berlin: Springer, 1984.- P.101-115-(LNCS; 164).

17. Clarke E.M., Brawne M.C., Emerson E.A. Using Temporal Logic for Automatic Verification of Finish State Systems // Logics and Models of Concurrent Systems. Proc. 1984 / Ed. by K.P.Apt. Berlin: Springer, 1985.- P.3-26.-(NATO ASI Series F; Vol.13).

18. Brawne M.C., Clarke E.M., Dill D.L. Automatic Verification of Sequential Circuits Using Temporal Logic // IEEE Transactions on Computers. 1986.-Vol/C-35, No. 12.- P. 1035-1044.

19. Kroger F. Temporal Logic of Programs. Berlin: Springer, 1985.- 148p. (EATCS Monographs on Theoreticals Computer Science; Vol.8).

20. Manna Z., Pnueli A. Verification of Concurrent Programs: The Temporal Framework // The Correctness Problem in Computer Science / R.S.Boyer and J.S.Moore (eds.). London: Academic Press, 1981.- P.215-273.

21. Логика и компьютер. Моделирование рассуждений и проверка правильности'программ. -М.: Наука, 1990,- 240с.

22. Э.М. Кларк, О. Грамберг, Д. Пелед. "Верификация моделей программ". Москва, 2002, изд-во МЦНМО, 415 с.

23. Fujita M., Kono S., Tanaka H. Aid to Hierarchical and Structured Logic Desine Using Temporal Logic and Prolog // IEE Proceedings. — 1986.-Vol.l33-E, No.5.- P.283-294.

24. Аникин A.B. Верификация проектов цифровых устройств с использованием метода Дейкстры-Гриса // Изв. ЛЭТИ: Сб. науч. тр./ Ленингр. элек-тротехн. ин-т им. В.И. Ульянова (Ленина).- Л. 1989.- Вып.415.-С.30-35.

25. Автоматное управление асинхронными процессами в ЭВ1Ч4 и дискретных системах / Под ред. В.И. Варшавского. — М.: Наука, 1986.- 400с.

26. Ачасова С.М., Вандман О.Л. Корректность параллельных вычислительных процессов.- Новосибирск: Наука, 1990.- 253с.

27. Варшавский В.И., Кишиневский М.А., Кондратьев А.Ю. Модели для спецификации и анализа процессов в асинхронных схемах // Изв. АН СССР. Техническая кибернетика.-1988.-№2,- С.171-190.

28. Котов В.Е. Сети Петри. М.:Наука, 1984.-160с.

29. Питерсон Дж. Теория сетей Петри и моделирование систем: Пер. с англ. -М.: Мир, 1984.- 264с.

30. Kreisel G., Krivine J.L. Elements of Mathematical Logic (Model Theory).- Amsterdam: North-Holland, 1971.- 232p.

31. Jahanian F., Mok A.K.-L. A Graph-Theoretical Approach for Timing Analysis and its Implementation // IEEE Transactions on Computers.- 1987.- Vol. C-36, No,8.- P.961-975.

32. Berthet C., Cerny E. An Algebraic Model for Asynchronous Circuit Verification // IEEE Transactions on Computers.- 1988.- Vol. 37, No,7.- P.835-837.

33. Александр Петренко, Елена Бритвина, Сергей Грошев, Александр Монахов, Ольга Петренко Тестирование на основе моделей // Открытые системы, #09/2003

34. Е. Clarke, О. Grumberg, D, Long Model Checking, In Springer-Verlag Nato ASI Series F, Volume 152, 1996

35. Зелковиц M., Шоу А., Гэннон Дж. Принципы разработки программного обеспечения. М.: Мир, 1982. - 368 с.

36. Липаев B.B. Отладка сложных программ. Методы, средства, технология. М.: Энергоатомиздат, 1993. -384 с.

37. Липаев В.В. Управление разработкой программных средств: Методы, стандарты, технология. М.: Финансы и статистика, 1993.

38. Майерс Г. Искусство тестирования программ. М.: Мир, 1982. 212с.

39. Грис. Д. Конструирование компиляторов для цифровых вычислительных машин. М.: Мир, 1975. - 544с.

40. Липаев В.В. Проектирование программных средств. М.: Высшая школа, 1990.

41. Андерсон Р. Доказательство правильности программ. —М.: Мир. — 1982.- 168с.

42. Бейбер Л.Р. Программное обеспечение без ошибок. М. Радио и связь. 1996. 173 с.

43. И.Б.Бурдонов, А.В.Демаков, А.С.Косачев, А.В.Максимов, А.К.Петренко Формальные спецификации в технологиях обратной инженерии и верификации программ.// Труды Института системного программирования Российской Академии наук. N 1, 1999.

44. Э. Дейкстра. Заметки по структурному программированию. //У. Дал, Э. Дейкстра, К. Хоор. Структурное программирование. М.: Мир, 1975.

45. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ. М.: Радио и связь, 1988.

46. Основы верификационного анализа безопасности исполняемого кода программ. / Матвеев В.А., Молотков C.B., Зегжда Д.П.,Мешков A.B., Семьянов П.В., Шведов Д.В. Под редакцией проф. Зегжды П.Д. СПб.: СПбГТУ, 1994. 58с.

47. Alur R., Henzinger T., Pei-Hsin Ho. Automatic symbolic verification of embedded systems //IEEE Trans, on Software Eng. 1996. N3.

48. Липаев B.B. Надежность программных средств. M.: СИНТЕГ, 1998,-232 с.

49. Lowry M Analytic Verification and Validation for Space Missions. NASA Ames Research Center http://is.arc.nasa.gov/AR/projects/AtnVrf.html

50. Черноножкин C.K. Меры сложности программ // Системная информатика. Новосибирск: Наука. Сиб. отд-ние, 1997. Вып. 5. Архитектурные, формальные и программные модели

51. Гацко Г. Тестирование ПО как один из элементов системы качества // Открытые системы. 1998. N6.

52. Коул Дженнифер, Горэм Томас, МакДональд Марк, Спарджеон Роберт. Принципы тестирования ПО // Открытые системы (Изд-во "Открытые системы"). 1998. № 2.

53. Никифоров В.В., Домарацкий Я.А. Системное тестирование программных изделий. // Программные продукты и системы. 1998. N 4. С. 40-46.

54. А.К. Поляков "Языки VHDL и VERILOG в проектировании цифровой аппаратуры" М., Солон-Пресс, 2003

55. М. R. A. Huth, M.D. Ryan. Logic in Computer Science: Modelling f and Reasoning about Systems. Cambridge University Press, 2002, 387 p.

56. Липаев B.B. Сопровождение и управление сложных программных средств. -М.: СИНТЕГ, 2006. -372с.

57. Проектирование цифровых вычислительных машин / С.А. Майоров, Г.И. Новиков, О.Ф. Немолочнов и др. Под ред. С.А. Майорова. М.: Высш.шк., 1972. 344 с.

58. Зыков А.Г., Немолочнов О.Ф., Виноградов Ю.Н., Поляков В.И. Верификация как средство отладки моделей различного уровня. «Известия вузов. Приборостроение»/ Том 46, №2, 2003, С.51-55.

59. Итерационно-рекурсивная модель вычислительных процессов, порождаемых программами / Немолочнов О.Ф., Зыков А.Г., Поляков В.И., Осовецкий Л.Г., Сидоров A.B. Кулагин B.C.- «Известия вузов. Приборостроение»/ Том 48, №12, СПб, 2005, С.14-20.

60. Деметрович Я., Кнут Е., Радо П. . Автоматизированные методы спецификации. М.: Мир, 1989).

61. В.Е. Котов, Л.А. Черкасова Исчисление процессов, в кн. «Системная информатика». Вып. 2, Новосибирск, «Наука», 1993.

62. M.K. Molloy Performance Analesis Using Stochastic Petri Nets // IEEE Transactions on Computers.- Vol. C-31, 1982, September

63. Стешенко В.Б. Примеры проектирования цифровых устройств с использованием языков описания аппаратуры / «Схемотехника», 2001, № 7, С. 42; №8, С.32; № 10, С.42; № 11, С.46.

64. Климович Ф., Соловьев В.В. Логическое проектирование цифровых систем на основе программируемых логических интегральных схем. М.: Радио и связь, 2008. 376 с.

65. Лаздин A.B., Немолочнов О.Ф. Оценка сложности графа функциональной программы / Научно-технический вестник СПБ ГИТМО (ТУ). Выпуск 6. Информационные, вычислительные и управляющие системы / Гл. ред. В.Н. Васильев. СПб.: СПбГИТМО (ТУ), 2002.

66. Немолочнов О.Ф. Методы технической диагностики / Методическое пособие / ЛИТМО, Ленинград, 1977 г.

67. Немолочнов О.Ф. Контроль и диагностика сочетаний неисправностей в комбинированных системах / УС и М, №4, Киев, 1973 г.

68. Майоров С.А., Новиков Г.И. Принципы организации цифровых машин. Д., «Машиностроение», 1974. 432 с.

69. Баранов С.И., Синёв В.Н. Автоматы и программируемые матрицы. Мн., «Выс. школа», 1980. 136 с.

70. Чжен Г., Мэннинг Е., Метц Г. Диагностика отказов цифровых вычислительных систем. Пер. с англ. под ред. И. Б. Михайлова. М., «Мир», 1972. 232 с.

71. Липаев В.В. Функциональная безопасность программных средств. Сер. Управление качеством. М.: Синтег, 2004.

72. Зыков А.Г., Немолочнов О.Ф., Поляков В.И. Универсальная модель последовательностных схем в САПР / Научно-технический вестник СПБ

73. ГИТМО (ТУ). Выпуск 6. Информационные, вычислительные и управляющие системы / Гл. ред. В.Н. Васильев.- СПб.: СПб ГИТМО (ТУ), 2002. с. 107-108.

74. Ope О. Теория графов. М.: «Наука», 1968. — 352с.

75. Карибский В.В., Пархоменко П.П., Согомонян Е.С., Халчев В.Ф. / Основы технической диагностики. Кн.1.- М.: Энергия, 1976

76. Графы и алгоритмы. Структуры данных. Модели вычислений: Учебник / В.Б. Алексеев, В.А. Таланов. М.: Интернет-Университет Информационных технологий; БИНОМ. Лаборатория знаний, 2006. - 320с.

77. Немолочнов О.Ф., Усвятский А.Е., Звягин В.Ф., Голыничев В.Н. Промышленная система автоматизации проектирования тестов.// УС и М. 1981. №5

78. Блохин В.Н., Голованевский Г.Л., Зыков А.Г., Немолочнов О.Ф. Доступная система контроля цифровых узлов и верификация логических модулей. / Сб. «ЭВМ в проектировании и производстве» / Вып. 4, «Машиностроение», 1989.

79. Зыков А.Г., Немолочнов О.Ф. Автоматная модель устройства управления в САПР при верификации проекта. / Межвузовский сборник научных трудов «Автоматизированное проектирование в радиоэлектронике и приборостроении», С.-Пб, ГЭТУ, 1994. С. 21-23.

80. Модель и примитивы покрытий вершин циклических вычислительных процессов / Немолочнов О.Ф., Зыков А.Г., Осовецкий Л.Г., Поляков В.И. //Известия вузов. Приборостроение. 2007. Том 50, №8, С. 18-23.

81. Тестирование логических неисправностей вычислительных процессов в программах / Немолочнов О.Ф., Зыков А.Г., Осовецкий Л.Г., Поляков В.И., Петров К.В. / Журнал «Информационные технологии» / №12, М., 2007, С.2-5.

82. Functional Verification of a Multiple-Issue, Out of Order, Superscalar Alpha Processor. DAC, 1998.