Моделирование распределенных систем и анализ их семантических свойств

• Автор: Соколов, Валерий Анатольевич
• Шифр специальности: 01.01.09
• Научная степень: Докторская
• Год защиты: 2006
• Место защиты: Ярославль
• Количество страниц: 319 с. : ил.

1 Структурированные системы переходов

1.1. Предварительные сведения

1.2. Системы помеченных переходов

1.3. Примеры вполне структурированных систем переходов

2 Счетчиковые машины

2.1. Счетчиковые машины Минского

2.2. Счетчиковые машины с потерями

2.3. Счетчиковые машины с обнулениями

и ошибками проверки на нуль

2.4. Недетерминированные счетчиковые

машины
3 Темпоральные свойства систем переходов
3.1. Метод проверки модели
3.2. Темпоральные свойства систем
переходов
4 Модели Dataflow - программ
4.1 Модели и свойства класса структурированных программ в языках потоков данных
4.2 О проблеме достижимости в графах потоков данных с очередями и стеками
5 Язык рекурсивно-параллельного программирования: семантика и приложение к алгебраическим вычислениям
5.1 Модель семантики рекурсивнопараллельных программ

5,2 Язык рекурсивно-параллельного программирования и его
применение к алгебраическим вычислениям
6 Моделирование и анализ протоколов
6.1 Протокол ТСР с адаптацией скорости
6.2 Модификация транспортного протокола ТСР с использованием метода динамических приоритетов
Заключение
Литература •
Приложение

Современный период развития информатики и вычислительной техники характеризуется широким использованием параллельных и распределенных систем, поведение которых отличается высокой степенью сложности. Это обстоятельство выдвигает новые задачи в области моделирования и анализа корректности таких систем. Многие существующие методы и средства анализа параллельных и распределенных систем, таких как, например, вычислительные машины и комплексы с параллельной и распределенной архитектурой, параллельные программы, протоколы передачи данных, модели технологических и бизнес-процессов, основаны на использовании помеченных систем переходов с конечным числом состояний, представляющих собой технически простое, но очень удобное и достаточно общее средство для моделирования параллельного поведения.
За последнее время отмечается резкое возрастание интереса исследователей к проблемам, связанным с разработкой методов моделирования и проверки корректности параллельных и распределенных систем, накоплено большое количество теоретических результатов и практического опыта в этой области. Среди отечественных исследований по спецификации, моделированию и анализу сложных (в т.ч., параллельных и распределенных) систем отметим работы H.A. Анисимова, О.Л. Банд-ман, И.Б. Вирбицкайте, В.В. Воеводина, Н.В. Евтушенко, В.А. Захарова, Ю.Г. Карпова, В.Е. Котова, И.А. Ломазовой, В.А. Непомнящего, А.К. Петренко, Р.Л. Смелянского, Л.А. Черкасовой, Н.В. Шилова.
При исследовании сложных систем зачастую приходится строить формальные модели, которые представляют собой системы переходов с бесконечным числом состояний. В этом случае многие средства анализа и верификации, производящие полный перебор пространства состояний, становятся неприменимыми. Тем не менее, для некоторых ограниченных классов систем с бесконечным числом состояний разными авторами были разработаны достаточно эффективные методы верификации (как, например, в работах P. Abdulla, K. Ceräns, A. Finkei, В. Jonsson, F. Möller,
• M - конечное множество сообщений (видов сообщений),
• 5 - конечное множество переходов, каждый из которых представляет собой набор вида {s,op,S2), где в и в2 - это управляющие состояния, а ор - метка одного из следующих видов:
- ст, где с£ С ит £ М,
- dm, где с£ С и т £ М,
- а, где а £ А.
Интуитивно, конечная управляющая часть системы £ = (5, so, А, С, М, 6) - это обычная помеченная система переходов с множеством состояний S, начальным состоянием so и правилами переходов 5. Канальная часть представлена множеством каналов-очередей С, каждый из которых может содержать строку сообщений, принадлежащих множеству М. Множество А обозначает множество взаимодействий с внешней средой. Каждый переход из 5 осуществляет внешнее взаимодействие из А или некоторую (внутреннюю) операцию над каналами, где
• переход вида (si,c!m,S2) меняет управляющее состояние si на состояние S2. добавляя при этом сообщение т в конец канала с,
• переход вида (si,c?m, S2) меняет управляющее состояние si на состояние S2, удаляя при этом сообщение т из начала канала с.
• переход вида (si, a,s2) меняет управляющее состояние si на состояние s2 без изменения содержимого каналов.
Рассмотрим FIFO-канальную систему как систему с потерями (Lossy Channel System). Для этого будем предполагать, что в любой момент времени возможна внезапная потеря сообщения из некоторого канала. Т.е. добавим новую операцию потери т(с, т) такую, что
• при переходе вида (s, т(с, m), s) происходит удаление сообщения т из канала с без изменения управляющего состояния.
Операционное поведение системы с потерями определяется посредством формализации интуитивного поведения системы как системы помеченной системы переходов с бесконечным числом состояний.
Пусть £ = (5, fr,A,C,M,S) - это система с ненадежными каналами. Глобальное состояние 7 системы £ представляет собой пару (s,w), где s £ S и и> : С -л М", Начальное глобальное состояние у0 системы £