Каталог / ТЕХНИЧЕСКИЕ НАУКИ

Формальная верификация процессора с устройствами поддержки виртуальной памяти

Диссертация

Автор: Далингер, Яков

Заглавие: Формальная верификация процессора с устройствами поддержки виртуальной памяти

Справка об оригинале: Далингер, Яков. Формальная верификация процессора с устройствами поддержки виртуальной памяти : диссертация ... кандидата технических наук : 05.00.00 / Далингер Яков; [Место защиты: Ун-т Саарланда] - Саарбрюккен, 2006 - Количество страниц: 152 с. ил. Саарбрюккен, 2006 152 c. :

Физическое описание: 152 стр.

Выходные данные: Саарбрюккен, 2006






Содержание:

1 Введение
11 Используемые обозначения
12 Среда формальных доказательств PVS
13 Базовые логические элементы
14 Виртуальная память
15 Декомпозиция доказательства
151 Уровень интерфейса памяти
152 Уровень интерфейса процессора
2 Блок поддержки виртуальной памяти
21 Спецификация MMU
211 Допущение для MMU
212 Гарантии MMU
22 Дизайн MMU
23 Корректность MMU
3 VAMP с поддержкой виртуальной памяти
31 Спецификация VAMP процессора
32 Имплементация процессора VAMP
321 Алгоритм Томасуло
322 Дизайн процессора VAMP
323 Имплементация блока памяти процессора VAMP
33 Критерий корректности
331 Планировочные функции
332 Инвариант корректности
333 Обзор доказательства
34 Корректность между прерываниями
341 Корректность блока памяти при чтении / записи
342 Выборка инструкций
35 Корректность с прерываниями
351 Полная корректность



Похожие работы:
  • Формальная семантика C-LIGHT программ и их верификация методом Хоара
  • Система трехуровневой управляемой виртуальной памяти УВП-3
  • Аппаратно-программные средства управления задачами и организация виртуальной памяти в системе с автоматическим распределением ресурсов
  • Когнитивная и формальная структура конструкций обусловленности
  • Формальная геометрия и алгебраические инварианты геометрических структур
  • Формальная и трансцендентальная логика в "Критике чистого разума" И. Канта
  • Формальная дифференциация лексико-семантических вариантов слова в русском языке
  • Формальная теория структурных моделей описания информационных систем и методы установления выводимости
  • Формальная модель контекстно-зависимых программных структур и их преобразований в применении к методологии Language-Driven Development
  • Исследование оптического вейвлет-процессора