Цена доставки диссертации от 500 рублей 

Поиск:

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

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

Диссертация

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

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

Справка об оригинале: Далингер, Яков. Формальная верификация процессора с устройствами поддержки виртуальной памяти : диссертация ... кандидата технических наук : 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 Полная корректность

Введение:
На текущий момент, существует много приложений где процессора используются в устройствах, критичных для жизни человека, например атомные электрические станции, самолеты, поезда, автомобили или медицинские приборы. Разработчики процессоров используют различные тесты для того чтобы обнаружить ошибки в них. Так как не исчерпывающие тесты пе покрывают все возможные случаи поведения процессора, процессора выпускаемые индустрией могут содержать ошибки. Формальная верификация все больше и больше признается единственной альтернативой, так как актуальные результаты в формальной верификации эквивалентны симуляции всех возможных случаев поведения процессора. Более того, это даже лучше чем симуляция потому, что можно получить корректность нескольких модулей сразу.В данной работе доказывается только корректность работы аппаратного обеспечения используемого в академической системе проекта Verisoft. Следует отметить, что ошибки программного обеспечения также могут быть причиной неправильного поведения системы. Поэтому, как доказательство корректности работы апнаратного уровня, так и доказательство корректности программного обеспечения необходимы, а доказательство корректности работы аппаратного уровня это только первый шаг на пути получения корректности полной компьютерной системы.К р а т к о е с о д е р ж а н и е глав В главе 1 рассматривается основная нотация, используемая во всей работе. Так же будут рассмотрены: система формальных доказательств, виртуальная память и основной подход к декомпозиции доказательств в данной работе.В главе 2 рассматривается конструкция неоптимизированного блока поддержки виртуальной памяти (ММи), который является аппаратной частью поддержки виртуальной памяти. Здесь же будет доказана корректность работы данного блока при нетривиальных условиях: данные в ячейках памяти И используемые для транслирования адреса не должны быть перезаписаны в течении всего запроса к MMU.В последней главе 4 обобпдаются результаты, проводится дискуссия о достоинствах и недостатках разработанной системы, представляется информация о работах других ученый в данном направлении, а также обсуждаются возможности для дальнейшей работы.