Содержание к диссертации
Введение 3
1 Структурированные системы переходов 19
-
Предварительные сведения 19
-
Системы помеченных переходов 26
-
Примеры вполне структурированных систем переходов . . 43
2 Счетчиковые машины 69
-
Счетчиковые машины Минского 70
-
Счетчиковые машины с потерями 73
-
Счетчиковые машины с обнулениями
и ошибками проверки на нуль 83
2.4. Недетерминированные счетчиковые
машины 94
3 Темпоральные свойства систем переходов 103
-
Метод проверки модели 103
-
Темпоральные свойства систем
переходов 125
4 Модели Dataflow - программ 148
-
Модели и свойства класса структурированных программ в языках потоков данных 148
-
О проблеме достижимости в графах потоков данных с очередями и стеками 173
5 Язык рекурсивно-параллельного программирования: се
мантика и приложение к алгебраическим вычислениям 190
5.1 Модель семантики рекурсивно-
параллельных программ 190
5.2 Язык рекурсивно-параллельного программирования и его
применение к алгебраическим вычислениям 206
6 Моделирование и анализ протоколов 222
-
Протокол TCP с адаптацией скорости 222
-
Модификация транспортного протокола TCP с использованием метода динамических приоритетов 234
Заключение 244
Литература 246
Приложение 263
Введение к работе
Современный период развития информатики и вычислительной техники характеризуется широким использованием параллельных и распределенных систем, поведение которых отличается высокой степенью сложности. Это обстоятельство выдвигает новые задачи в области моделирования и анализа корректности таких систем. Многие существующие методы и средства анализа параллельных и распределенных систем, таких как, например, вычислительные машины и комплексы с параллельной и распределенной архитектурой, параллельные программы, протоколы передачи данных, модели технологических и бизнес-процессов, основаны на использовании помеченных систем переходов с конечным числом состояний, представляющих собой технически простое, но очень удобное и достаточно общее средство для моделирования параллельного поведения.
За последнее время отмечается резкое возрастание интереса исследователей к проблемам, связанным с разработкой методов моделирования и проверки корректности параллельных и распределенных систем, накоплено большое количество теоретических результатов и практического опыта в этой области. Среди отечественных исследований по спецификации, моделированию и анализу сложных (в т.ч., параллельных и распределенных) систем отметим работы Н.А. Анисимова, О.Л. Банд-ман, И.Б. Вирбицкайте, В.В. Воеводина, Н.В. Евтушенко, В.А. Захарова, Ю.Г. Карпова, В.Е. Котова, И.А. Ломазовой, В.А. Непомнящего, А.К. Петренко, Р.Л. Смелянского, Л.А. Черкасовой, Н.В. Шилова.
При исследовании сложных систем зачастую приходится строить формальные модели, которые представляют собой системы переходов с бесконечным числом состояний. В этом случае многие средства анализа и верификации, производящие полный перебор пространства состояний, становятся неприменимыми. Тем не менее, для некоторых ограниченных классов систем с бесконечным числом состояний разными авторами были разработаны достаточно эффективные методы верификации (как, например, в работах P. Abdulla, К. Cerans, A. Finkel, В. Jonsson, F. Moller, Ph. Schnoebelen [57, 112, 159]. В частности, оказалось, что метод проверки модели (Model Checking), широко используемый при автоматической верификации систем с конечным числом состояний, может быть применим для некоторых классов систем с бесконечным числом состояний и подмножеств темпоральных логик. Примерами формальных моделей, являющихся системами переходов с бесконечным числом состояний и позволяющих описывать параллельные и распределенные системы, являются магазинные автоматы [17, 56], сети Петри [21], ВРР (Basic Parallel Processes) [94], LCS (Lossy Channel Systems - системы с каналами, теряющими сообщения) [61, 62], Real-Time Automata(aBTOMaTbi реального времени) [71] и др.
Метод Model Checking - один из наиболее перспективных подходов к решению проблемы верификации [95]. В качестве языков спецификации для выражения свойств систем при этом подходе используются темпоральные логики. Задача проверки модели состоит в определении выполнимости для системы, заданной формальным образом (в виде формальной модели), свайгт»-, исписанною формулой темпоральной логики.
Исследования систем переходов с бесконечным числом состояний были мотивированы теорией формальных языков и грамматик [132, 56, 17]. Во-первых, в этой теории бесконечные языки описываются конечными грамматиками, а во-вторых, некоторые проблемы для языков, например, проблема эквивалентности регулярных языков, являются разрешимыми. Следовательно, не все проблемы систем переходов с бесконечным числом состояний неразрешимы. По аналогии с теорией формальных языков были введены новые формализмы для описания бесконечных систем переходов.
Классическим примером является магазинный автомат. В теории формальных языков он используется для описания контекстно-свободных языков. Но этот автомат может быть также рассмотрен как модель системы переходов с бесконечным числом состояний. Каждое управляющее состояние (множество которых конечно) вместе с содержимым стека (магазина) описывает состояние системы переходов. Поскольку размер стека не ограничен, то может быть бесконечно много различных состояний системы. Состояние меняется, когда автомат принимает терминальный символ. Однако это можно интерпретировать как совершение действия системой и переход её в другое состояние.
Указанные формализмы, как и многие другие, могут быть рассмотрены как вполне структурированные системы помеченных переходов [57, 112].
