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

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

Автор: Коннов, Игорь Владимирович

Шифр специальности: 05.13.11

Научная степень: Кандидатская

Год защиты: 2008

Место защиты: Москва

Количество страниц: 198 с. ил.

Артикул: 4130705

Автор: Коннов, Игорь Владимирович

Стоимость: 250 руб.

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

Оглавление
Введение .
Проверка корректности программ.
Цель диссертационной работы
, 1
Актуальность работы
Основные результаты
Структура работы.
Глава 1. Постановка задачи
1.1. Модели распределнных систем .
1.2. Задача верификации моделей распределнных систем .
1.3. Задача верификации параметризованных моделей распределнных систем .
Глава 2. Обзор литературы
2.1. Аналитические методы редукции . . .
2.2. Методы абстракции.
2.3. Символьные методы.
2.4. Методы, основанные на поиске инварианта.
2.5. Выводы, выбор мегода и декомпозиция задачи .
Глава 3. Основные определения
3.1. Размеченные системы переходов.
3.2. Асинхронная параллельная композиция
3.3. Описание топологии распределнных систем с помощью сетевых грамматик
3.4. Темпоральные логики.
3.5. Конечные и бесконечные блоки
3.6. Выводы.
Глава 4. Новые отношения симуляции .
4.1. Блочная симуляция .
4.2. Квазиблочная симуляция.
4.3. Полублочная симуляция .
4.4. Выводы.
Глава 5. Метод сетевых инвариантов для случая асинхронных параметризованных систем .
5.1. Метод сетевых инвариантов с использованием квазиблочной и блочной симуляций .
5.2. Алгоритм построения полублочной симуляции.
5.3. Оценки сложности
5.4. Выводы
Глава 6. Практическая реализация и проверка протокола резервирования ресурсов .
6.1. Архитектура системы СЬеАРБ
6.2. Протокол резервирования ресурсов .
6.3. Предыдущие работы по верификации протокола .
6.4. Параметризованная модель
6.5. Верификация параметризованной модели
6.6. Проверка свойств модели протокола
6.7. Выводы
Заключение
Литература


Указаны способы абстракции [2, , , , , , ] для определённых классов систем. Как будет показано в обзоре, наиболее перспективными методами, настраиваемыми на различные виды топологии параметризованных систем, являются методы, основанные на поиске инвариантов, и символьные методы. Символьные методы верификации параметризованных систем могут потребовать участия эксперта для переработки модели и указания дополнительных подсказок. Примечательно, что примеры успешного применения метода, основанного на поиске инвариантов, относятся к классам распределенных систем синхронно-взаимодействующих процессов (9—, , , ), хотя метод инвариантов использовался и для систем асинхронно-взаимодействующих процессов в работах [, , ]. Помимо верификации моделей с произвольным числом однотипных процессов алгоритмы решения задачи РМС позволяют проводить редукцию моделей с большим числом однотипных процессов к моделям с малым числом процессов. Таким образом, решение задачи РМС имеет практический смысл даже тогда, когда рассматриваются модели с фиксированным, но очень большим числом процессов. В этом случае задача, требующая недоступных на практике вычислительных ресурсов, может быть сведена к практически решаемой задаче. Таким образом, задача верификации параметризованных моделей распределённых систем актуальна. Однако при разработке таких методов и средств желательно сохранить основное преимущество метода МС — свойство автоматической верификации модели. Необходимо, чтобы для верификации параметризованной модели не требовалась существенная перестройка модели, использованной при верификации средствами МС, или участие эксперта. Предложен новый метод верификации систем асинхронно-взаимодействующих процессов, позволяющий автоматически вычислять конечные инварианты параметризованных моделей и сводить задачу верификации бесконечных параметризованных моделей к задаче верификации конечных моделей. На основе предложенного метода разработаны новые алгоритмы верификации параметризованных систем асинхронно-взаимодсйствующих процессов, сочетающие методы верификации моделей программ и проверки отношений симуляции между моделями программ. На основе предложенного метода и алгоритмов разработана и реализована экспериментальная система автоматической верификации программ, с помощью которой доказана корректность поведения ряда распределенных алгоритмов и сетевых протоколов, применяющихся на практике. Работа состоит из введения, шести глав, заключения и двух приложений. В первой главе обсуждаются требования, предъявляемые к моделям распределённых систем, а также задача верификации моделей распределённых систем. На основе этого обсуждения формулируется задача верификации параметризованных моделей распределённых систем и формируются требования к методам решения этой задачи. Во второй главе приводится обзор и сравнительный анализ работ, в которых предлагаются решения задачи верификации параметризованных моделей распределённых систем. На основании критериев, предъявляемых к решению задачи с учётом целей настоящей работы, выбирается метод инвариантов, на основе которого разрабатывается предлагаемый в работе метод верификации параметризованных моделей распределённых систем. С учётом выбранного базового метода формулируется декомпозиция задачи. В третьей главе описываются основные понятия теории формальной верификации моделей программ: размеченные системы переходов, темпоральные логики, сетевые грамматики. В терминах введённых понятий формулируется математическая задача проверки выполнимости спецификации, заданной формулой темпоральной логики, на параметризованных моделях программ, представленных посредством размеченных систем переходов и сетевых грамматик. Исследованы основные свойства этих отношений. Показано, что введённые отношения обладают необходимым набором свойств для решения задачи верификации параметризованных моделей распределённых систем с использованием метода инвариантов. В пятой главе описывается модификация метода инвариантов с использованием отношений симуляции, введённых в четвёртой главе.

Рекомендуемые диссертации данного раздела

28.06.2016

+ 100 бесплатных диссертаций

Дорогие друзья, в раздел "Бесплатные диссертации" добавлено 100 новых диссертаций. Желаем новых научных ...

15.02.2015

Добавлено 41611 диссертаций РГБ

В каталог сайта http://new-disser.ru добавлено новые диссертации РГБ 2013-2014 года. Желаем новых научных ...


Все новости

Время генерации: 0.235, запросов: 244