Содержание к диссертации
Введение 3
Глава 1
Предварительные понятия ..9
1.1 Развертки сетей Петри. 9
1.1.1.. Ветвящиеся процессы 9
Определения разверток сетей Петри. 10
Методы обнаружения тупиков 12
1.2 Раскрашенные сети Петри 13
Общие определения 14
Симметрия и эквивалентность 16
Раскрашенные сети Петри со временем 18
Модель интервального времени 18
Модель временных штампов 19
1.3 Метод проверки моделей 21
Логика линейного времени. 22
Логика мю-исчисления 23
Алгоритм проверки моделей для логики линейного времени 24
Алгоритм проверки моделей для логики мю-исчисления 26
Глава 2
Развертки раскрашенных сетей Петри. 27
Ветвящийся процесс для раскрашенных сетей Петри. 27
Определения и основные свойства разверток ....32
Алгоритмы построения разверток 34
Алгоритмы обнаружения тупиков 41
Глава 3
Развертки раскрашенных сетей Петри,
расширенных эквивалентностью и временем. 42
Применение эквивалентности в развертках 42
Развертки сетей с интервальным временем... 44
Развертки сетей с временными штампами 49
Глава 4
Метод проверки моделей для раскрашенных сетей Петри,
базирующийся на их развертках 55
Метод проверки моделей и обоснование его корректности 55
Применение метода проверки моделей к сетям,
расширенным свойством эквивалентности 60
4.3 Применение метода проверки моделей для временных сетей 63
Модель интервального времени 63
Модель временных штампов 64
Глава 5
Реализация методов проверки моделей
для раскрашенных сетей Петри. 66
5.1 Системы верификации раскрашенных сетей Петри 66
5.1.1 Система PNV 66
5.1.2 Реализация метода проверки
моделей с использованием разверток. 68
5.2 Экспериментальные результаты 69
Задача об обедающих философах 70
Битовый протокол 72
Кольцевой протокол 76
Протокол "Отправитель - получатель" 80
Заключение .82
Литература 83
Введение к работе
Верификация распределенных систем является быстро развивающейся областью современного программирования. В связи с всевозрастающей ролью сетевых соединений данная область имеет большое практическое значение. Ввиду большой сложности многих реальных распределенных систем вопрос о правильности их работы является нетривиальной задачей. Обнаружение ошибок в рассматриваемых системах математическими методами и доказательная проверка корректности их работы являются основными целями верификации распределенных систем. Естественный подход к проблеме верификации состоит в моделировании распределенных систем конечными автоматами или сетями Петри и последующей верификации полученных моделей.
Теории и приложениям сетей Петри посвящена богатая литература, см., например, [9]. В России велись исследования по моделированию, спецификации и верификации распределенных систем с использованием сетей Петри. Отметим, в частности, работы О.Л. Бандман [2,3] по спецификации поведения сетевых протоколов, Н.А. Анисимова [15] по спецификации протоколов, В.А. Соколова [12] по анализу паралельных программ и И.Б. Вирбицкайте [4] по использованию техники частичного порядка для верификации временных сетей Петри.
Среди наиболее важных подходов к верификации сетей Петри можно выделить симуляцию работы сети и анализ ее пространства состояний. При симуляции работа сети изучается пошаговым методом в ручном или полуавтоматическом режимах. Хотя многие ошибки в работе сети могут быть обнаружены на этапе симуляции, доказательная проверка корректности работы сети может быть получена при полном моделировании работы сети и проведении так называемой проверки моделей. Метод проверки моделей заключается в описании требуемых свойств системы на языках логических спецификаций и доказательстве истинности (или ложности) данных спецификаций на построенном пространстве состояний системы.
Последние два десятилетия метод проверки моделей активно развивался в работах многих авторов и показал себя как эффективное и многообещающее средство для верификации распределенных систем. Благодаря своей естественности и возможности быть интегрированным в среду разработки и анализа распределенных систем, метод проверки моделей был принят в качестве одного из стандартов для верификации спецификаций систем, описанных на каком-либо формальном языке. В качестве входных данных для процедуры проверки моделей поступают описание самой системы (чаще всего задаваемое в виде некоторой структуры с конечным числом состояний) и логическая спецификация (обычно, формула временной логики), описывающая проверяемое свойство системы. В качестве формализмов для описания структуры системы чаще всего используются такие модели, как структуры Крипке и помеченные системы переходов [19, 20, 51]. Активно используемые логические спецификации подразделяются на логики линейного времени (LTL) и логики ветвящегося времени. Среди наиболее используемых логик ветвящегося времени следует отметить логику Хеннесси-Милнера, логику модального мю-исчисления, базирующуюся на теории неподвижных точек, и логику вычислимых деревьев (CTL - Computational Tree Logic) [51]. Методы проверки моделей подразделяются на локальную и глобальную проверку моделей. При локальной проверке моделей по заданной логической спецификации и некоторому участку (состоянию) системы необходимо определить, является ли данная спецификация истинной на заданном участке или нет. При глобальной проверке моделей по заданной логической спецификации и описанию системы необходимо определить те состояния системы, в которых формула логической спецификации является истинной. Методы проверки моделей предоставляют полностью автоматический способ решения данных задач. Обзор современного состояния теории проверки моделей можно найти, например, в работе [19].
К сожалению, при полном моделировании работы сети мы сталкиваемся с так называемой "проблемой взрыва числа состояний" (state explosion problem). Эта проблема состоит в том, что при росте размеров рассматриваемой сети, ее полная модель достаточно быстро становится необозримо большой. Это не позволяет надеяться на построение полной модели для реальных протоколов. Отдельным и, как это следует из вышесказанного, достаточно важным направлением верификации распределенных систем является разработка методов, направленных на решение проблемы взрыва числа состояний. Среди таких методов можно выделить следующие: метод упрямых множеств (stubborn set method), использование двоичных разрешающих диаграмм (symbolic binary decision diagrams ), методы, основанные на частичном порядке (partial order methods), а также использование симметрии и эквивалентности на рассматриваемых моделях [54].
Рассмотренный в данной работе подход относится к методам, основанным на использовании частичного порядка. В качестве модели при проверке логических спецификаций вместо полного графа достижимости/ используется так называемая развертка сети Петри. Развертки сетей Петри является относительно новым и интенсивно развивающимся направлением в области верификации сетей Петри. Данный метод позволяет во многих случаях существенно уменьшить размер модели, не теряя при этом свойств рассматриваемой сети.
Среди различных расширений стандартных сетей Петри выделяются сети Петри высокого уровня — раскрашенные сети Петри (РСП) [35, 36], для которых развит теоретический аппарат, накоплен значительный опыт использования и реализована система симуляции и анализа Design/CPN [46]. В РСП вместо обычных фишек используются типизированные знаковые элементы. Также есть возможность задания функций на дугах и переходах. Это расширение позволяет выражать в достаточно компактном виде сложные системы, не теряя при этом возможностей применять методы, разработанные для стандартных сетей Петри. Данная работа посвящена применению метода проверки моделей с использованием разверток к раскрашенным сетям Петри.
Использование разверток для анализа стандартных сетей Петри было предложено МакМилланом в работе [48]. Было предложено использовать конечный префикс максимального ветвящегося процесса вместо полного графа достижимости. Размер развертки является экспоненциальным в общем случае, и в последующих работах были предложены некоторые улучшения определений и алгоритмов построения развертки [25, 45]. Так в работе [25] было предложено рассматривать обобщенное понятие порядка на конфигурациях, и с его помощью, был предложен критерий финитизации, являющийся оптимальным для одно-безопасных сетей Петри. В работе [45] было показано, что для п-безопасных сетей Петри данный критерий не является оптимальным и было предложено существенное улучшение критерия для п-безопасных сетей Петри. В работе [45] также был предложен алгоритм построения развертки, линейно зависящий от произведения числа мест и переходов развертки.
Первоначально МакМиллан предложил использовать развертки для анализа достижимости и обнаружения тупиков. Эти методы были улучшены в последующих работах [31, 50]. В работе [31] предложено улучшение метода определения достижимости данного состояния сети. В работе [50] дается метод обнаружения тупиковых состояний с использованием системы неравенств, описывающих рассматриваемую сеть Петри. Дж. Эспарца в работе [24] предложил метод проверки моделей для одно-безопасных сетей Петри и логики S4 с использованием развертки. В работе [16] для сетей Петри с интервальным временем была построена развертка и применен алгоритм проверки моделей Эспарцы. В работе [57] Ф. Валнер предложил алгоритм проверки моделей для LTL логики, основанный на развертках сети Петри. В его работе известный теоретико-автоматный подход к верификации LTL формул [56] был перенесен на одно-безопасные сети Петри без тупиковых состояний. Этот подход был развит в последующих работах
[14, 22, 27, 28, 33]. На последнем этапе алгоритма Валнера строится дополнительный граф, состоящий из точек сечения рассматриваемой развертки. В работах [27, 28] была показана возможность модификации алгоритма, позволяющая избежать построения данного дополнительного графа и описана реализация данного подхода с приведением экспериментальных результатов. Работы [14, 33] посвящены теоретическим аспектам методов проверки моделей с использованием разверток. В работе [33] были доказаны некоторые сложностные оценки алгоритмов проверки моделей с использованием разверток. Работа [14] посвящена рассмотрению возможностей применения методов развертки к неограниченным сетям Петри. Стоит также отметить работу [26], в которой метод развертки был применен к синхронизированному произведению двух сетей Петри.
Развертка РСП без применения критериев финитизации в общем случае была рассмотрена в работе [55] для использования её в методе упрямых множеств. В этой работе, помимо отсутствия финитизации, также использовалось старое представление раскрашенных сетей Петри. Все это заставило автора сделать вывод о неэффективности использования разверток РСП, и в его дальнейших работах было показано, как применять метод упрямых множеств для РСП без построения развертки. Развертки РСП не рассматривались более в литературе. Хотя для стандартных сетей Петри были развиты критерии финитизации, эффективные алгоритмы построения разверток, техника работы со свойством достижимости и по обнаружению тупиков, а также алгоритмы проверки моделей для логики LTL, возможность применения данной техники к РСП оставалась открытым вопросом.
Цель диссертации состоит в разработке эффективных методов и алгоритмов верификации моделей распределенных систем, базирующихся на раскрашенных сетях Петри. Достижение цели связано с решением следующих задач:
- Разработка эффективных методов построения разверток РСП без временных
конструкций.
Исследование метода развертки для РСП, расширенных спецификациями эквивалентности и временными конструкциями.
Разработка метода проверки моделей с использованием разверток РСП, расширенных спецификациями эквивалентности и временными конструкциями.
Реализация разработанных методов и проведение экспериментов, подтверждающих, что метод развертки РСП является эффективным и может быть применен для верификации моделей распределенных систем.
Методы исследований базируются как на применении аппарата сетей Петри, так и на алгоритмах и методах теории проверки моделей. В области сетей Петри используются теория раскрашенных сетей Петри и методы разверток стандартных сетей Петри.
В диссертациионой работе формально строится максимальный ветвящийся процесс для РСП, используя их современное представление [35, 36], и конструктивно доказывается его существование. В работе определены развертки РСП как конечный префикс максимального ветвящегося процесса, полученный с помощью некоторого критерия финитизации, для которых доказываются свойства конечности, безопасности и полноты. Первое свойство дает нам конечность развертки, полученной при применении трех заданных критериев финитизации. Второе гарантирует отсутствие в развертках лишней информации о поведении РСП. Третье свойство дает нам существование во всех трех типах развертки полной информации о графе достижимости РСП. Методы финитизации, разработанные для стандартных сетей Петри, были применены для построенного максимального ветвящегося процесса РСП. В работе описаны два алгоритма построения разверток РСП и даны оценки сложности данных алгоритмов. Первый алгоритм является удобным средством для проведения теоретических рассуждений, в то
время как второй алгоритм является эффективным с точки зрения практики. Показано, как применять методы обнаружения тупиков, описанные в [50], к РСП. Методы работы с развертками интервально-временных сетей Петри [16] также формально применены к интервально-временным РСП. Следующим логичным шагом было применение методов проверки моделей, развитых для стандартных сетей Петри, к РСП. В диссертационной работе описана основанная на состояниях семантика LTL для РСП и разработан метод проверки моделей для логики LTL и РСП с использованием разверток. Метод позволяет эффективно проверять многие свойства, выразимые в логике линейного времени, для раскрашенных сетей Петри. Корректность полученного алгоритма формально доказана. Также показана возможность применения данного алгоритма к РСП с интервальным временем.
Вся описанная выше работа связана с перенесением методов, разработанных для стандартных сетей Петри на РСП. Однако, описанные в [35, 36] РСП имеют два существенные расширения. Во-первых, благодаря развитому аппарату работы с типами данных (цветами), имеются большие возможности по определению спецификаций симметрии и эквивалентности для РСП, основанные на цветовых значениях. Новым шагом, сделанным в данной работе, является разработка методов развертки РСП, расширенных спецификацией . эквивалентности. Теории построения разверток с использованием отношения эквивалентности не существовало ранее также и для стандартных сетей Петри, хотя некоторый шаг в этом направлении был сделан в работе [53]. Использование таких разверток РСП позволяет дополнительно существенно уменьшить размер рассматриваемой модели. В работе также показано, как можно использовать отношение эквивалентности при проведении проверки моделей с применением разверток. Второй особенностью РСП, отсутствующей в стандартной модели сетей Петри, является применение специальной временной модели, так называемой модели временных штампов. В диссертации показывается возможность применения методов развертки к РСП с временными штампами, а также возможность применения к ним метода проверки моделей для логики LTL. Заметим здесь, что получаемые развертки для РСП с временными штампами являются, в общем случае, бесконечными. Та же проблема возникает и при рассмотрении графа достижимости модели РСП с временными штампами [36]. В работе [36] было предложено использовать спецификации эквивалентности по времени для финитизации графа достижимости. В диссертации предлагается использовать аналогичный подход при построении разверток. Здесь основные методы, развитые в работе, а именно, развертки РСП, развертки РСП, расширенных временными конструкциями, и развертки РСП, расширенные спецификациями эквивалентности, применяются одновременно. В диссертации также показана возможность применения метода проверки моделей к РСП, расширенным спецификациями эквивалентности и временной моделью, основанной на временных штампах.
Практическая часть данной работы состоит в применении методов проверки моделей к раскрашенным сетям Петри. Данная часть включает применение стандартного метода проверки моделей для логики мю-исчисления к РСП и реализацию описанного в работе метода проверки моделей для LTL логики с использованием разверток РСП. Для применения первого подхода была реализована система PNV. В системе PNV процесс верификации РСП является полностью автоматическим и требует задания спецификации сети и формул во входных языках системы. Реализованная система проверки моделей с использованием разверток является прототипной реализацией и требует выполнения некоторых операций вручную. Цель реализации данной системы была показать принципиальную возможность и целесообразность использования данного метода на практике и дать несколько примеров верификации моделей распределенных систем. В дипломной работе [13] описана полная реализация системы проверки моделей для РСП с
применением разверток, не использующая отношение эквивалентности и временные конструкции, которая базируется на предложенных в данной диссертации методах.
Практическая ценность данных исследований заключается в том, что разработанный метод проверки моделей на базе разверток РСП во многих случаях оказался эффективнее известных методов, базирующихся на других формализмах. Введение спецификации эквивалентности позволяет дополнительно существенно уменьшить размер рассматриваемого пространства состояний. Проведенные эксперименты подтверждают целесообразность использования описанного подхода для верификации моделей распределенных систем.
Апробация, работы проведена на следующих международных научных конференциях:
International Conference on Parallel Computing in Electrical Engineering (PARELEC 2002), Warsaw, Poland.
4th International Conference of Perspectives of System Informatics (PSI'01), Novosibirsk,
Russia, 2001.
3. 5th International Workshop on Concurrency, Specification and Programming, Warsaw,
Poland, 2001.
4. Четвертый Сибирский Конгресс no Прикладной и Индустриальной Математике
(ИНПРИМ - 2000), Новосибирск, Россия, 2000.
Кроме того, полученные результаты; обсуждались на семинарах лаборатории теоретического программирования ИСИ СО РАН и кафедры систем информатики НГУ.
Публикации. По теме диссертации опубликовано 10 научных работ.
Структура работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы из 57 наименований. Содержание составляет 85 страниц. Работа включает 26 иллюстраций и 4 таблицы.
Работа состоит из следующих частей: в первой главе изложены предварительные понятия и результаты, используемые в данной работе. Раздел 1.1 посвящен краткому изложению теории разверток для стандартных сетей Петри. Раздел 1.2 является введением в раскрашенные сети Петри, как они описаны в работе [35]. В разделе 1.3 описаны логика линейного времени ( LTL ), логика мю-исчисления и алгоритмы проверки моделей для обеих логических систем. Вторая глава посвящена изложению теории развертки для раскрашенных сетей Петри. В разделах 2.1 и 2.2 даны определения и доказаны основные свойства максимального ветвящегося процесса и разверток РСП. В разделе 2.3 приведены алгоритмы построения разверток РСП. Раздел 2.4 посвящен применению методов обнаружения тупиков с использованием разверток к РСП. В следующей, третьей главе, методы развертки РСП применены к РСП, расширенным свойствами эквивалентности (раздел 3.1) и двумя временными моделями, интервальной моделью времени по Мерлину (раздел 3.2) и моделью временных штампов, предложенной в работах К. Йенсена (раздел 3.3). В четвертой главе метод проверки моделей для логики линейного времени применен к разверткам РСП (раздел 4.1) и к расширениям РСП спецификациями эквивалентности и симметрии (раздел 4.2) и двумя временными моделями (раздел 4.3). Пятая, последняя, глава работы описывает реализации двух систем проверки моделей для РСП, систему PNV, реализующую стандартный подход к реализации метода проверки моделей для РСП (раздел 5.1), и прототипную реализацию системы проверки моделей с использованием разверток для РСП (раздел 5.2). В разделе 5.3 приведены результаты экспериментов, проведенных с использованием данных двух систем.
