Исследование и разработка методов верификации протоколов распределенных систем на основе бисимуляционной эквивалентности сетей Петри

• Автор: Поступальский, Павел Алексеевич
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 1997
• Место защиты: Владивосток
• Количество страниц: 131 с. : ил.

Содержание
Введение

1 Задача верификации протоколов распределенных систем

1.1 Распределенные системы.

1.1.1 Эталонная модель взаимодействия открытых систем

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

1.2.1 Методы анализа логической корректности . . .

1.2.2 Задача верификации в терминах эталонной модели ВОС

1.2.3 Требование к формальной модели для верификации протоколов

1.3 Обзор формальных моделей.

1.4 Методология полной верификации протоколов

1.4.1 Спецификация протокола объектами сети Петри.
1.4.2 Построение модели верификации .
1.4.3 Сравнение спецификации сервиса и его логической реализации.
1.5 Автоматизированная система верификации.
1.5.1 Обзор автоматизированных систем, использующих бисимуляционную эквивалентность
1.5.2 Требования к автоматизированной системе верификации .
2 Методы верификации протоколов
2.1 Сети Петри
2.2 Верификация протоколов
2.3 Проверка помеченных сетей Петри на бисимуляцион
ную эквивалентность.
2.4 Построение сокращенного графа достижимости
2.5 Распределенная бисимуляционная эквивалентность . .
3 Автоматизированная система разработки спецификаций
3.1 Подсистема базового редактора.
3.1.1 Термины графичесого интерфейса с пользователем .
3.1.2 Инструментальная Панель Базового редактора
3.1.3 Меню Базового редактора.
3.2 Подсистема архитектурного редактора.
3.2.1 Инструментальная Панель Архитектурного редактора .
3.3 Подсистема верификации и анализа логической корректности .
3.3.1 Реализация алгоритма построения дерева достижимости.
3.3.2 Реализация алгоритма проверки на бисимуляционную эквивалентность
4 Практическое применение методов и средств
4.1 Дуплексный Бпротокол.
4.2 Протокол альтернативного бита.
4.3 Верификация протоколов альтернативного бита и Бпротокола.
Заключение
ЛИТЕРАТУРА


В то же время необходимо отметить, что указанная проблема верификации все еще не получила достаточно удовлетворительного решения. Под ней часто понимается доказательство отсутствия в исследуемых системах некоторого набора свойств логической корректности, таких как отсутствие тупиковых состояний, непродуктивных циклов, прием песпе-цифицированных команд и др. Такой анализ, хотя часто и является полезным, все же не гарантирует полной корректности протокола, и, в частности, отсутствия в них ошибок других типов. Другим недостатком, в основном связанным с использованием алгебраических теорий параллельных процессов, таких как ССБ, ТСЭР, АСР, является недостаточно адекватная интерпретация параллельности, не позволяющая, в частности, представлять одновременное выполнение параллельных событий. В то же время практические задачи по разработке распределенных систем выдвигают все более серьезные требования к средствам и методам верификации протоколов, гарантирующие их полную логическую корректность и, как следствие, правильное функционирование реализуемого телекоммуникационного оборудования и его программного обеспечения. Эти обстоятельства свидетельствуют об актуальности проблемы исследования и разработки методов полной верификации протоколов распределенных систем, а также реализации на их основе соответствующих автоматизированных средств. Связь с планами отраслей наук и народного хозяйства. Исследование и разработка методов анализа и синтеза протоколов сетей ЭВМ”, N гос. Формальные методы и средства разработки программного обеспечения распределенных вычислительных систем”, N гос. Основы композициональной теории сетей Петри”, грант -3-2. Композициональныс методы разработки сетевых протоколов”, грант 7. Цель работы. Целью диссертационной работы является разработка средств верификации протоколов распределенных систем на основе композициональных сетей Петри. Разработка методологических основ полной верификации протоколов с использованием композициональных сетей Петри. Разработка методов верификации протоколов на основе проверки шаговой бисимуляционной эквивалентности помеченных сетей Петри. Разработка автоматизированной системы, реализующая предложенную методологию полной верификации протоколов. Практическое применение и экспериментальная проверка разработанных инструментальных средств и методов верификации. Методы исследования базируются на применении аппарата теории сетей Петри, методов алгебраических теорий параллельных процессов, теории множеств. При реализации использовались технологии объектно-ориентированного программирования. Научная новизна работы заключается в предложении методологии полной верификации протоколов на основе аппарата компози-циональных сетей Петри. Применение в качестве формальной модели сетей Петри с хорошими возможностями представления параллельности и асинхронности позволяет обеспечить адекватность спецификации верифицируемых протоколов. Практическая ценность работы. Предложенные методы и инструментальные средства имеют ярко выраженный практический интерес и направлены на повышение эффективности разработки протоколов, обеспечивая их полную логическую корректность и соответствие между требуемой и реально предоставляемой функциональностью протокола. Реализация результатов работы. Материалы диссертационной работы использовались в учебном процессе на кафедре автоматизации научных исследований МФТИ и факультете математики и компьютерных технологий наук Дальневосточного государственного университета. Предложенные методы и инструментальные средства внедрены в Дальневосточной морской академии имени адмирала Невельского и Институте проблем морских технологий ДВО РАН, что подтверждено соответствующими документами. Апробация работы. V совещание по распределенным вычислительным системам и сетям (3-) (Калининград, ); Всесоюзная школа-семинар по вычислительным сетям (Алма-Ата, ); Дальневосточная математическая школа (Находка, ). Института автоматики и процессов управления ДВО РАН в - гг. Публикация результатов работы. По материалам диссертации опубликовано печатных работ.