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

• Автор: Зыков, Анатолий Геннадьевич
• Шифр специальности: 05.13.12
• Научная степень: Кандидатская
• Год защиты: 2008
• Место защиты: Санкт-Петербург
• Количество страниц: 154 с. : ил.

Оглавление
Введение
Глава 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 Концептуальная итерационнорекурсивная модель 1ЯМО
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.
Заключение.
Литература


При структурной верификации устанавливается соответствие структур, отображаемых двумя описаниями, при функциональной (параметрической) - проверяется соответствие процессов функционирования и выходных параметров, отображаемых сравниваемыми описаниями. Структурная верификация связана с меньшими затратами вычислительных ресурсов, чем функциональная. Поэтому последняя часто выполняется не в полном объеме и после того, как проверено соответствие структурных свойств. Примером структурной верификации служит установление соответствия системы электрических межсоединений на печатной плате и в принципиальной электрической схеме, заданных своими топологическими моделями в виде графов. Верификация в этом случае сводится к установлению изоморфизма графов. Функциональная верификация в данном примере выполняемся путем анализа переходных процессов с учетом перекрестных помех и задержек сигналов в длинных линиях, определяемых конструктивным исполнением электронного блока. Согласно Модели зрелости процесса разработки (Capability Maturity Model Integration) "верификация" определяется следующим образом: Верификация обеспечивает соответствие набора результатов работы требованиям, которые для них заданы [2]. Верификация в самом общем виде предполагает установление соответствия между различными объектами. Сами объекты могу т задаваться математическими моделями одного уровня либо моделями разного уровня представления [3]. В [4] предложена общая схема верификации (рис. Рис. Эта схема метода верификации состоит из нескольких этапов. На первом этапе требования извлекаются из нормативных документов и систематизируются. В результате получается каталог требований, в котором требования сформулированы максимально однозначно, требования классифицированы, и, возможно, установлены связи между отдельными требованиями. Каталог требований используется на последующих этапах. Второй этап нацелен на представление требований в формальном виде. Требования из каталога записываются с использованием того или иного математического формализма. Такая запись требований называется формальной спецификаций или формальной моделью. На третьем этапе на основе построенной модели автоматизированным образом генерируются тесты. В зависимости от задачи тесты могут либо быть просто тестовыми данными, либо дополнительно содержать оракул для автоматического вынесения вердикта о корректности наблюдаемого поведения объекта. В результате исполнения тестов строятся отчёты о тестировании. В них содержится информация о том, насколько наблюдаемое поведение объекта соответствует формальной модели. Определим некоторые понятия и определения, связанные с процессом тестирования, как составной части верификации. Эти определения распространяются на тестирование как ап паратуры, так и программ. Тестирование - процесс выполнения программы с целью обнаружения ошибки. Тестовые данные — входы, которые используются для проверки системы. Тестовая ситуация (test case) - входы для проверки системы и предполагаемые выходы в зависимости от входов, если система работает в соответствии с ее спецификацией требований. Хорошая тестовая ситуация - та ситуация, которая обладает большой вероятностью обнаружения пока еще необнаруженной ошибки. Удачный тест - тест, который обнаруживает пока еще необнаруженную ошибку. Ошибка - действие программиста на этапе разработки, которое приводит к тому, что в программном обеспечении содержится внутренний дефект, который в процессе работы программы может привести к неправильному результату. Отказ - непредсказуемое поведение системы, приводящее к неожидае-мому результату, которое могло быть вызвано дефектами, содержащимися в ней. Ыа рис. Несмотря на кажущуюся схожесть, термины «тестирование», «верификация» и «валидация» означают разные уровни проверки корректности работы вычислительной системы. В [8] предложено следующее определение этих понятий. Тестирование — вид деятельности в процессе разработки, связанный с выполнением процедур, направленных на обнаружение (доказательство наличия) ошибок (несоответствий, неполноты, двусмысленностей и т. Процесс тестирования относится в первую очередь к проверке корректности программной или аппаратной реализации системы, соответствия реализации требованиям, т. Рис.