Глонина Алевтина Борисовна Анализ конфигураций модульных вычислительных систем для проверки выполнения ограничений реального времени : Глоніна Алевтина Борисівна Аналіз конфігурацій модульних обчислювальних систем для перевірки виконання обмежень реального часу

Краткое описание

Глонина Алевтина Борисовна Анализ конфигураций модульных вычислительных систем для проверки выполнения ограничений реального времени
ОГЛАВЛЕНИЕ ДИССЕРТАЦИИ
кандидат наук Глонина Алевтина Борисовна
Введение

Глава 1. Постановка задачи проверки выполнения ограничений реального времени

для МВС

1.1. Устройство и примеры МВС

1.2. Конфигурация МВС и ограничения реального времени

1.3. Актуальность задачи

1.4. Формальная постановка задачи

Глава 2. Обобщенная модель функционирования МВС

2.1. Выбор математического аппарата для построения модели

2.2. Формальное определение сетей временных автоматов с остановкой таймеров

2.3. Обобщенные сети временных автоматов с остановкой таймеров

2.4. Описание обобщенной модели функционирования МВС

2.5. Метод построения экземпляра модели по описанию конфигурации МВС

2.6. Построение временной диаграммы функционирования МВС

2.7. Разработанные модели компонентов МВС

2.8. Оценки сложности построения и прогона экземпляра модели МВС

Глава 3. Доказательство корректности моделей МВС

3.1. Понятие корректности моделей МВС и метод ее обоснования

3.2. Верификация моделей компонентов МВС

3.3. Корректность модели МВС в целом

3.4. Детерминированность моделей МВС

Глава 4. Инструментальная система проверки выполнения ограничений реального

времени для конфигураций МВС

4.1. Требования к инструментальной системе

4.2. Состав и схема работы инструментальной системы

4.3. Библиотека моделирования сетей временных автоматов с остановкой таймеров

4.4. Интеграция с САПР «Планировщик ИМА»

Глава 5. Экспериментальное исследование разработанных методов и средств

5.1. Цели и методика экспериментального исследования

5.2. Анализ результатов экспериментов

5.3. Выводы

Заключение

Стр.

Список литературы

Приложение А. Разработанные модели компонентов МВС

А.1. Модель планировщика ядра

А.2. Модели планировщиков работ разделов

А.3. Модель функциональной задачи

A.4. Модель виртуального канала

Приложение Б. Утверждения о выборе диапазонов значений параметров и

переменных при верификации

Б.1. Проблема выбора диапазонов значений параметров и переменных при верификации

Б.2. Временные параметры

Б.3. Параметры, задающие размеры массивов

Б.4. Индексные параметры

Б.5. Переменные интерфейса

Б.6. Совместное применение доказанных утверждений

Приложение В. Автоматы-наблюдатели для проверки выполнения требований

корректности к моделям компонентов МВС

B.1. Автоматы для требований к моделям планировщиков раздела

В.2. Автоматы для требований к моделям функциональных задач

В.3. Автоматы для требований к моделям планировщиков ядра

В.4. Автоматы для требований к моделям виртуальных каналов

В.5. Автоматы для требований к моделям конкретных типов компонентов МВС

Приложение Г. Результаты экспериментов

Введение