«ВЕРИФИКАЦИЯ ПАРАМЕТРИЗОВАННЫХ МОДЕЛЕЙ РАСПРЕДЕЛЁННЫХ СИСТЕМ ...»

МОСКОВСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

им. M.В. Ломоносова

На правах рукописи

КОННОВ Игорь Владимирович

ВЕРИФИКАЦИЯ ПАРАМЕТРИЗОВАННЫХ МОДЕЛЕЙ

РАСПРЕДЕЛЁННЫХ СИСТЕМ

05.13.11 — математическое и программное обеспечение

вычислительных машин, комплексов и компьютерных сетей

ДИССЕРТАЦИЯ

на соискание ученой степени кандидата физико-математических наук

Научные руководители:

доктор физ.-мат. наук, академик РАЕН, профессор Р. Л. Смелянский;

кандидат физ.-мат. наук, доцент В. А. Захаров.

Mосква — Оглавление Введение................................... Проверка корректности программ.................... Цель диссертационной работы...................... Актуальность работы........................... Основные результаты........................... Структура работы............................. Глава 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. Архитектура системы CheAPS................... 6.2. Протокол резервирования ресурсов................ 6.3. Предыдущие работы по верификации протокола........ 6.4. Параметризованная модель..................... 6.5. Верификация параметризованной модели............. 6.6. Проверка свойств модели протокола............... 6.7. Выводы................................ Заключение................................. Литература................................. Приложение А. Некоторые существующие отношения на LTS А.1. Трассовая эквивалентность..................... А.2. Бисимуляционная эквивалентность (бисимуляция)....... А.3. Прореженная бисимуляция..................... А.4. Ветвящаяся бисимуляция...................... Приложение Б. Детали реализации экспериментальной систе­ Б.1. Описание алгоритма построения полублочной симуляции... Б.3. Подсистема порождения моделей по сетевой грамматике.... Б.4. Подсистема построения полублочной симуляции......... 3.1 Диграммы LTS процессов типа Root, Inner, Leaf......... 4.1 Пример LTS, находящихся в отношении блочной симуляции.. 4.3 Взаимосвязь между путями в.......... 4.4 Диаграмма путей пункта (2а).................... 4.5 Диаграмма путей пункта (2б).................... 4.6 Критерий полублочной симуляции................. 6.1 Архитектура системы проверки параметризованных систем... 6.2 Время построения полублочной симуляции с различными опти­ 6.3 Потребление памяти при построении полублочной симуляции с А.1 Модели 1 и 2 находятся в отношении бисимуляции..... А.2 LTS 1 и 2 находятся в отношении симуляции......... А.3 Отсутствие симуляции для LTS, отличающихся уровнем аб­ А.4 Процессы и и два экземпляра параметризованного семейства Б.1 Сгенерированный граф модели из пяти процессов........ Б.2 Архитектура подсистемы проверки симуляции.......... Б.3 Признаки нестабильности пар состояний............. Проверка корректности программ В настоящее время сложилось несколько подходов к проверке правиль­ ности программ: тестирование, теоретико-доказательный подход и верифика­ ция моделей программ. ©Igor V. Konnov, PhD Thesis, Наиболее распространённым методом является тестирование. При тести­ ровании на вход программе подаются заранее приготовленные тестовые дан­ ные и проверяется соответствие результата, выданного программой, ожида­ емому. Важным свойством, используемом при тестировании, является свой­ ство детерминированности алгоритма. В случае распределённых программ, использующих несколько процессов и выполняющихся на нескольких вычис­ лительных устройствах, поведение программы становится существенно неод­ нозначным. В этом случае для проверки поведения программы в ходе вычис­ ления могут использоваться средства трассировки.

Как заметил Дейкстра [100]: «Тестирование программ может использо­ ваться для демонстрации наличия ошибок, но оно никогда не покажет их от­ сутствие». Методы верификации направлены на доказательство утверждений о свойствах поведения программы или результатов её работы. Этот подход к проверке правильности программ был впервые предложен в работах А.А. Ля­ пунова [103, 104], Т. Хоара [40], Э. Дейкстры [100], Пратта [81] и Флойда [25].

Наиболее грандиозная задача верификации программ, известная как «Grand challenge», сформулирована в работе Хоара [41]. В этой работе описы­ вается задача создания верифицирующего компилятора, т.е. такого компиля­ тора, который проверяет корректность программы при трансляции. Там же приводится список достижений, благодаря которым Хоар считает, что тех­ нология разработки и верификации программ является достаточно зрелой для проведения исследований по созданию верифицирующего компилятора.

В работе приводятся требования к решению задачи. Формулировка задачи ис­ пользуется в качестве общей цели для исследовательских групп, работающих в области валидации и верификации программ. ©Igor V. Konnov, PhD Thesis, Методы верификации программ, использующие теоретико-доказатель­ ный подход, основываются на средствах автоматического доказательства тео­ рем (САДТ, theorem prover, «прувер») [72, 73, 83, 90]. Описание программы представляется в виде множества логических утверждений. Спецификация программы также представляется в виде утверждения. САДТ строит дока­ зательство выполнимости спецификации, исходя из утверждений, описываю­ щих проверяемую программу.

К сожалению, при использовании САДТ в процессе построения доказа­ тельства может потребоваться участие эксперта. Одной из наиболее трудных задач, возникающих при верификации программ с помощью САДТ, является задача порождения инварианта цикла [40]. Инвариант цикла требуется при проверке выводимости постусловия функции из предусловия. Несмотря на значительный прогресс в этой области [51, 53], верификация большинства программ всё ещё требует привлечения эксперта.

Верификация программы с использованием логических утверждений, по­ строенных непосредственно на основании исходных кодов программы, увели­ чивает сложность процесса доказательства. В тоже время некоторые фраг­ менты кода могут быть несущественными для проверки выделенных свойств программы. Свойства программы могут быть проверены на модели програм­ мы, более простой, чем исходная программа. Группа методов, основанных на верификации моделей (Model Checking, MC) [102], использует компромисс­ ный подход между полноценной верификацией программы и тестированием, использующим формальную проверку свойств.

В группе методов MC по исходной программе строится модель в виде си­ стемы переходов, т.е. множества состояний модели, множества её начальных состояний и отношения переходов на множестве состояний. Для каждого со­ стояния также задаются значения булевых переменных модели. Как правило, переменные модели являются абстракцией выделенного множества структур данных исходной программы. Спецификация задаётся с помощью формулы темпоральной логики. С помощью темпоральных логик удобно описываются свойства поведения программы: реакции процесса на событие, связи между событиями, пребывания процесса в безопасных состояниях и пр. Благодаря тому, что число состояний модели конечно, задача проверки выполнимости формулы темпоральной логики на модели алгоритмически разрешима. Более того, найдены полиномиальные (относительно числа состояний модели) ал­ горитмы проверки спецификации на модели. Выполнимость спецификации на всех трассах модели, исходящих из начальных состояний, анализируется с помощью алгоритмов поиска в пространстве состояний. ©Igor V. Konnov, PhD Thesis, Первые примеры успешного применения MC относятся к проверке мо­ делей аппаратных схем. В дальнейшем методы MC успешно применялись для проверки моделей сетевых протоколов, распределённых алгоритмов. В последние годы методы MC стали применяться и для верификации после­ довательных программ. В 2007 году за изобретение первых алгоритмов MC основоположники группы методов MC Э. Кларк, А. Эмерсон и Ж. Сифакис получили премию Тьюринга.

Применение методов MC ограничивает целый ряд недостатков, прису­ щих этой группе методов:

сложность построения адекватной модели, эффект «комбинаторного взрыва», требование конечности модели.

Применение группы методов MC связано с нетривиальным вопросом по­ строения корректной и адекватной модели. Модель строится для проверки соответствия исходной программы заданному набору спецификаций, поэто­ му модель должна быть адекватной, т.е. отражать все свойства исходной программы, необходимые для проверки спецификаций. Также модель долж­ на быть корректной для выбранного набора свойств, т.е. поведение модели должно соответствовать поведению исходной программы с учётом выбран­ ных свойств. От выбора свойств исходной программы, переносимых на мо­ дель, зависит адекватность модели проверяемому набору спецификаций и практическая применимость группы методов MC.

Если корректность модели можно гарантировать с помощью ограниче­ ний на методы построения модели по программе, то адекватность может быть проверена только после того, как проведена верификация модели. Для построения корректной модели могут использоваться методы автоматическо­ го порождения моделей (Model Extraction [45]) по заданной программе, а автоматическое построение адекватной модели достигается за счёт комби­ нирования методов булевой абстракции с итеративной верификацией моде­ лей [12, 14, 87]. Такой подход к построению моделей получил название Counter Example Guided Abstraction Refinement. В случае неудачной проверки по­ строенной модели проводится уточнение модели с помощью САДТ. Стоит заметить, что в данном случае комбинируются средства MC и САДТ. Соот­ ветственно, гарантия полностью автоматической проверки моделей, вообще говоря, исчезает, так как не во всех случаях САДТ способны выдать доказа­ тельство запрашиваемого утверждения.

Эффект «комбинаторного взрыва» связан с экспоненциальным ростом пространства состояний при линейном росте числа взаимодействующих про­ цессов. Последствиями экспоненциального роста пространства состояний ста­ новятся высокие требования к объему памяти, используемой верификатором моделей, и долгое время проверки модели. Для сжатия проверяемого множе­ ства состояний используются символьные способы представления моделей, например, двоичные разрешающие диаграммы (Binary Decision Diagrams, BDD) [19]. В символьном представлении модели выражаются с помощью BDD, которые реализуют функции алгебры логики. При поиске в простран­ стве состояний вместо перебора состояний используются операции над функ­ циями. Алгоритмы верификации моделей с помощью BDD могут быть зна­ чительно эффективнее явного перебора состояний в том случае, когда BDD системы переходов модели и промежуточных результатов остаются компакт­ ными [65]. Для моделей аппаратных схем представление модели в виде BDD даёт хороший коэффициент сжатия по отношению к явному представлению множеств. Модели распределённых программ сжимаются несколько хуже, так как в распределённых программах используется асинхронное взаимодей­ ствие. ©Igor V. Konnov, PhD Thesis, Для борьбы с «комбинаторным взрывом» при верификации моделей про­ грамм используются методы редукции частичных порядков [43, 76, 77]. В этих методах проверяется достаточное подмножество множества всех трасс. Такое подмножество вычисляется на основании зависимостей между переходами процессов модели. Типы проверяемых зависимостей выявляются эмпириче­ ски. Удачный выбор правил редукции может существенно ускорить алгоритм верификации модели [43].

Третьей проблемой применения группы методов MC является требова­ ние конечности числа состояний проверяемой модели. Алгоритмы MC гаран­ тированно завершаются и эффективно работают именно на моделях с конеч­ ным числом состояний. При попытке обобщения задачи верификации мето­ дами MC с целью проверки систем с бесконечными множествами состояний возникает два направления: верификация моделей с бесконечным числом со­ стояний и верификация параметризованных моделей.

При верификации моделей с бесконечным числом состояний (Infinite State-Space Model Checking) в описании модели могут присутствовать пере­ менные с неограниченными типами данных, а порождаемая по описанию си­ стема переходов обладает бесконечным множеством состояний. Для решения этой задачи используются комбинации символьных методов верификации мо­ делей и методов доказательства теорем [4, 18, 24, 30, 32, 36, 48, 63, 66, 69, 80, 85, 89].

Задача верификации параметризованных моделей (Parameterized Model Checking, PMC) возникает при рассмотрении моделей распределённых си­ стем, в которых число однотипных взаимодействующих процессов зависит от начальной конфигурации системы и может быть сколь угодно большим. Как известно, увеличение числа вычислителей не всегда приводит к линейному росту производительности распределённой системы. Аналогично, выводы о выполнимости спецификации, полученные для конфигурации с одним числом процессов, нельзя переносить на конфигурации с другим числом процессов, не приводя дополнительной аргументации. Решение задачи PMC позволяет убедиться в выполнимости проверяемых спецификаций при масштабирова­ нии распределённой программы, т.е. при росте числа взаимодействующих процессов. ©Igor V. Konnov, PhD Thesis, При фиксированном числе процессов может быть построена модель рас­ пределённой системы с конечным числом состояний. Однако число взаимо­ действующих процессов неограниченно, и множество моделей с различным числом процессов бесконечно. Проверка произвольных моделей с фиксиро­ ванным числом процессов не даёт гарантии выполнимости проверяемого свой­ ства при увеличении числа взаимодействующих процессов, а все модели про­ верить невозможно.

В задаче PMC рассматриваются распределённые системы взаимодейству­ ющих процессов. В этих системах присутствует фиксированное число стати­ ческих процессов и неограниченное число однотипных процессов. Так как число однотипных процессов не ограничено, то по распределённой системе может быть построено бесконечное семейство моделей. Каждая модель соот­ ветствует конфигурации системы с фиксированным числом процессов. Для проверки свойств распределённой системы необходимо проверить специфика­ цию на всех моделях бесконечного семейства. Способы решения задачи для некоторых случаев параметризованных моделей приведены в работах [2, 7– 11, 15, 17, 20–23, 28, 47, 49, 54–59, 61, 62, 64, 68, 71, 85, 86, 88, 89, 92, 93, 95, 97].

В последующих разделах будет проведён краткий анализ этих методов. Имен­ но задаче верификации параметризованных моделей распределённых систем посвящена настоящая диссертационная работа.

Цель диссертационной работы Цель диссертационной работы — разработка и анализ алгоритмов вери­ фикации параметризованных моделей распределённых программ для провер­ ки свойств распределённых программ с произвольным числом однотипных асинхронно-взаимодействующих процессов.

При этом предъявляются следующие требования к решению:

разрабатываемые алгоритмы должны опираться на существующие ал­ горитмы верификации моделей с конечным числом состояний;

разрабатываемые алгоритмы должны использовать существующие спо­ собы описания моделей с фиксированным числом процессов. В таком случае модели, разработанные и верифицированные с применением уже существующих средств поддержки методов MC, могут быть параметри­ зованы и верифицированы с помощью разработанных алгоритмов без значительных доработок моделей.

Актуальность работы В области вычислительной техники исследуются классы систем, пара­ метризованных по числу взаимодействующих компонентов. К числу таких систем относятся:©Igor V. Konnov, PhD Thesis, распределённые алгоритмы [60, 91]: волновые алгоритмы, распределе­ ния ресурсов, взаимного исключения доступа к критической секции, из­ брания лидера (leader election), обнаружения завершения (termination detection), согласованного принятия транзакции (distributed commit);

сетевые протоколы [109]: кольцо с маркером, протоколы маршрутиза­ ции, протоколы обеспечения качества сервиса, широковещательные про­ аппаратные схемы: аппаратные схемы управления доступом к шине при различном числе клиентских устройств, протоколы обеспечения коге­ рентности кэшей [38].

В дальнейшем под словами «распределённый алгоритм» мы будем пони­ мать как системы из первого, так и из второго пункта.

Довольно часто при построении модели распределённой системы, кото­ рая может потенциально содержать любое количество однотипных процессов, ограничиваются моделью с небольшим, фиксированным числом процессов.

При этом предполагается, что свойства, проверенные на модели с фикси­ рованным числом процессов, автоматически масштабируются для моделей с бльшим числом процессов. Однако этот приём не является вполне кор­ ректным: известны примеры, когда спецификация была верна на модели с одним числом процессов и нарушалась при изменении числа процессов [102, c. 161], [7].

Это означает, что для верификации параметризованных моделей про­ грамм недостаточно проверить спецификацию на нескольких моделях с фик­ сированным числом процессов: необходимо обоснование масштабируемости проверенной спецификации на остальные модели. Так как число процессов в моделях не ограничено, то спецификация должна быть проверена на беско­ нечном семействе моделей с конечным числом состояний. В работе [1] пока­ зано, что в общем случае задача PMC сводится к задаче останова машины Тьюринга и, следовательно, алгоритмически неразрешима.

Тем не менее, для некоторых практически интересных классов парамет­ ризованных моделей задача PMC может быть решена. Так, показана разре­ шимость задачи для однонаправленных колец с маркером одного типа [20], колец с произвольным типом маркера и дополнительными ограничениями на LTS процесса [23, 93], симметричных систем с глобальными предусло­ виями переходов [21, 24], широковещательных систем [21, 22, 61], систем с произвольной топологией и одним маркером [95]. Предложены различ­ ные полуразрешающие процедуры: подходы, основанные на поиске инвари­ антов [9–11, 52, 55, 64, 86, 97]; подходы, основанные на проверке достижимых состояний регулярных моделей [2, 30, 59, 88]; символьные методы верифи­ кации [4, 80, 85]. Указаны способы абстракции [2, 36, 47, 50, 57, 61, 95] для определённых классов систем. ©Igor V. Konnov, PhD Thesis, Как будет показано в обзоре, наиболее перспективными методами, на­ страиваемыми на различные виды топологии параметризованных систем, яв­ ляются методы, основанные на поиске инвариантов, и символьные методы.

Символьные методы верификации параметризованных систем могут потребо­ вать участия эксперта для переработки модели и указания дополнительных подсказок. Примечательно, что примеры успешного применения метода, осно­ ванного на поиске инвариантов, относятся к классам распределённых систем синхронно-взаимодействующих процессов [9–11, 52, 55, 97], хотя метод инва­ риантов использовался и для систем асинхронно-взаимодействующих процес­ сов в работах [11, 64, 86].

Помимо верификации моделей с произвольным числом однотипных про­ цессов алгоритмы решения задачи PMC позволяют проводить редукцию мо­ делей с большим числом однотипных процессов к моделям с малым числом процессов. Таким образом, решение задачи PMC имеет практический смысл даже тогда, когда рассматриваются модели с фиксированным, но очень боль­ шим числом процессов. В этом случае задача, требующая недоступных на практике вычислительных ресурсов, может быть сведена к практически ре­ шаемой задаче.

Таким образом, задача верификации параметризованных моделей рас­ пределённых систем актуальна. Однако при разработке таких методов и средств желательно сохранить основное преимущество метода MC — свой­ ство автоматической верификации модели. Необходимо, чтобы для верифи­ кации параметризованной модели не требовалась существенная перестройка модели, использованной при верификации средствами MC, или участие экс­ перта.

Основные результаты 1. Предложен новый метод верификации систем асинхронно-взаимодей­ ствующих процессов, позволяющий автоматически вычислять конеч­ ные инварианты параметризованных моделей и сводить задачу верифи­ кации бесконечных параметризованных моделей к задаче верификации конечных моделей.

2. На основе предложенного метода разработаны новые алгоритмы вери­ фикации параметризованных систем асинхронно-взаимодействующих процессов, сочетающие методы верификации моделей программ и про­ верки отношений симуляции между моделями программ.

3. На основе предложенного метода и алгоритмов разработана и реали­ зована экспериментальная система автоматической верификации про­ грамм, с помощью которой доказана корректность поведения ряда рас­ пределенных алгоритмов и сетевых протоколов, применяющихся на практике.

Структура работы

Работа состоит из введения, шести глав, заключения и двух приложений.

В первой главе обсуждаются требования, предъявляемые к моделям рас­ пределённых систем, а также задача верификации моделей распределённых систем. На основе этого обсуждения формулируется задача верификации па­ раметризованных моделей распределённых систем и формируются требова­ ния к методам решения этой задачи.

Во второй главе приводится обзор и сравнительный анализ работ, в ко­ торых предлагаются решения задачи верификации параметризованных мо­ делей распределённых систем. На основании критериев, предъявляемых к решению задачи с учётом целей настоящей работы, выбирается метод инва­ риантов, на основе которого разрабатывается предлагаемый в работе метод верификации параметризованных моделей распределённых систем. С учётом выбранного базового метода формулируется декомпозиция задачи.

В третьей главе описываются основные понятия теории формальной ве­ рификации моделей программ: размеченные системы переходов, темпораль­ ные логики, сетевые грамматики. В терминах введённых понятий формули­ руется математическая задача проверки выполнимости спецификации, задан­ ной формулой темпоральной логики, на параметризованных моделях про­ грамм, представленных посредством размеченных систем переходов и сете­ вых грамматик.©Igor V. Konnov, PhD Thesis, В четвёртой главе вводятся новые отношения симуляции: квазиблочная, блочная и полублочная. Исследованы основные свойства этих отношений. По­ казано, что введённые отношения обладают необходимым набором свойств для решения задачи верификации параметризованных моделей распределён­ ных систем с использованием метода инвариантов.

В пятой главе описывается модификация метода инвариантов с исполь­ зованием отношений симуляции, введённых в четвёртой главе. Предлагается алгоритм построения отношения полублочной симуляции, с помощью которо­ го проводится поиск инварианта параметризованной модели распределённой системы. Указываются возможные способы оптимизации алгоритма для по­ нижения сложности.

Практическая применимость разработанных методов, алгоритмов и про­ грамм верификации параметризованных моделей распределённых систем проверена на примере нескольких моделей распределённых программ и прото­ колов. В шестой главе приводится архитектура экспериментальной системы верификации параметризованных моделей распределённых систем. Там же описывается параметризованная модель сетевого протокола резервирования ресурсов. Приводятся результаты численного эксперимента по верификации параметризованной модели при помощи разработанной экспериментальной системы верификации.

В заключении формулируются основные результаты работы и возмож­ ные направления развития.

В приложении А описываются отношения частичного порядка (симуля­ ции) и эквивалентности (бисимуляции) на размеченных системах переходов, играющие важную роль в методе инвариантов, используемом для решения задачи.©Igor V. Konnov, PhD Thesis, В приложении Б приводится подробное описание алгоритма построения полублочной симуляции, доказательство его корректности, обоснование оце­ нок сложности; далее приводится описание экспериментальной системы вери­ фикации параметризованных моделей распределённых систем. Описываются способы оптимизации реализации алгоритмов в экспериментальной системе.

1.1. Модели распределённых систем В научной литературе встречаются различные формальные и нефор­ мальные описания распределённых систем (Distributed System, DS) [60, 91, 107, 110]. Характерным свойством DS является наличие взаимодействующих компонентов системы. В настоящей работе основное внимание уделяется ве­ рификации моделей программных систем, поэтому далее под компонентами DS понимаются взаимодействующие процессы. Процессы выполняются на од­ ном или нескольких вычислительных устройствах. В общем случае, вычисли­ тельные устройства могут быть физически удалены друг от друга. В данной работе задержка, возникающая при передаче данных, не учитывается, и вза­ имодействие процессов считается мгновенным.

Примерами распределённых систем служат:

программно-аппаратные комплексы: компьютерные сети [109], борто­ вые системы самолетов [106], системы телефонной связи [27], автома­ тические системы управления движением поездов [105];

программные комплексы: распределённые алгоритмы [60, 91], распре­ делённые базы данных [101, гл. 21], распределённые файловые систе­ При построении модели DS важен выбор моделируемых аспектов систе­ мы. В настоящей работе основные характеристики DS трактуются следую­ щим образом:

Время. Глобальные часы в системе отсутствуют. Состояния процессов из­ меняются дискретно при возникновении событий. События считаются атомарными. События в системе подразделяются на два вида: локаль­ ные и коммуникационные. Локальное событие связано с одним процес­ сом, а коммуникационное — с двумя взаимодействующими процессами.

Параллелизм. Процессы в системе выполняются асинхронно с чередовани­ ем (interleaving).

Взаимодействие. Все взаимодействия процессов осуществляются с помо­ щью синхронного обмена сообщениями (rendezvous). Обмен сообщени­ ями с очередями фиксированного размера моделируется дополнитель­ ными процессами.

Топология. При исследовании распределённых систем, в особенности пара­ метризованных по числу процессов, и построении моделей важную роль играет вид топологии коммуникационной сети распределённой систе­ мы. Примерами видов топологии коммуникационной сети DS служат:

кольцо, шина, -мерный куб. В данной работе рассматриваются моде­ ли распределённых систем, вид топологии которых описывается кон­ текстно-свободными сетевыми грамматиками [10, 64, 86]. В дальнейшем для DS, параметризованных по числу процессов, под словом «тополо­ гия» мы будем понимать вид топологии коммуникационной сети DS.

Сбои. Так как узлы распределённой системы могут быть физически удале­ ны друг от друга, возможна ситуация, в которой часть узлов становится недоступной для других узлов из-за неисправности каналов связи или самих узлов. В данной работе рассматриваются модели, в которых уз­ лы не выходят из строя, а сообщения не теряются и не искажаются.

Моделирование сбоев в системе может осуществляться добавлением со­ стояний сбоя в узлы.©Igor V. Konnov, PhD Thesis, Для анализа поведения распределённой системы часто в качестве моде­ ли DS используются системы переходов (Transition System, TS) [79]. Клю­ чевыми составляющими системы переходов являются понятие состояния и перехода. Состояние системы переходов является абстракцией состояния рас­ пределённой системы. В состоянии TS отражены значения структур данных процессов DS, необходимых для анализа её поведения. Из состояния модели может осуществляться переход в одно или несколько следующих состояний.

Переход соответствует локальному или коммуникационному событию моде­ лируемой DS.

Системы переходов могут сопровождаться разметкой состояний и/и­ ли переходов. В этом случае говорят о размеченных системах переходов (Labelled Transition System, LTS) [79, 102]. В данной работе используются LTS с разметкой состояний значениями булевых переменных и разметкой пе­ реходов названиями коммуникационных действий.

При построении модели строятся LTS процессов DS. Модель всей DS образуется в результате параллельной композиции LTS процессов: = · · ·, где 1,..., — LTS процессов DS.©Igor V. Konnov, PhD Thesis, В методах MC спецификации DS обычно задаются с помощью формул темпоральной логики [102]. Формулы темпоральной логики описывают вре­ менные свойства вычислений (последовательностей переходов) модели. Наи­ большее применение в методе MC получили логики ветвящегося времени (Computational Tree Logic, линейного времени (Linear Time Logic, 1.2. Задача верификации моделей распределённых Задача верификации моделей распределённых систем методами MC фор­ мулируется следующим образом:

Задача 1 (Верификации моделей методами MC, Model Checking Problem, MCP). Дана модель = 1 · · ·, где 1,..., — LTS процессов.

Задана формула (спецификация) темпоральной логики относительно пе­ ременных модели. Необходимо проверить выполнимость формулы на модели (обозначение: |= ).

1.3. Задача верификации параметризованных моделей распределённых систем В данной работе рассматривается обобщение задачи MCP. Методы MC применяются к моделям DS, состоящих из конечного множества процессов, заданных в виде LTS. Как отмечалось во введении, существуют DS, число процессов в которых зависит от начальной конфигурации или настройки DS, а множество таких конфигураций бесконечно. При этом число процессов не меняется во время работы DS.

Для распределённых систем, в которых число процессов зависит от на­ чальной конфигурации, могут быть построены модели с конечным числом состояний для каждой начальной конфигурации системы. Так как множе­ ство начальных конфигураций бесконечно, то и множество моделей с раз­ личным числом процессов бесконечно. Верификация нескольких, случайно выбранных моделей, из этого множества не гарантирует выполнимость спе­ цификации на всех моделях множества. Для таких систем рассматривается задача, в общем случае формулируемая следующим образом [102, гл. 15]:

Задача 2 (Верификации параметризованных моделей, Parameterized Model Checking Problem, PMCP). Дано бесконечное семейство конечных моделей = { }, параметризованное по параметру N. Задана формула (спе­ цификация) темпоральной логики. Необходимо проверить выполнимость формулы на всех моделях семейства, т.е. |= для всех.

Постановка задачи PMCP требует уточнения, так как в общей постанов­ ке явно не указывается способ задания семейства и спецификации. В настоящей работе рассматривается вариант PMCP1 задачи PMCP:

Задача 3 (PMCP1). Дано бесконечное семейство конечных моделей = { }, параметризованное по параметру N. Каждая модель = 1 · · · состоит из LTS фиксированного процесса и экземпляров про­ тотипа процесса — LTS процессов. Зафиксировано конечное множество N индексов наблюдаемых процессов, экземпляров прототипа процесса.

Спецификация темпоральной логики задаётся относительно переменных выделенных процессов1,, и переменных процесса. Необходимо про­ верить выполнимость формулы на всех моделях семейства, т.е. |= для всех.

Замечание 1.1. Рассматривают также вариант PMCP2 задачи PMCP, в кото­ рой задаются свойства с квантором всеобщности по номеру процесса [3, 10, 86] или нескольким номерам процессов [20]. Как показано в работе [20], в случае симметричности формулы и моделей семейства, такой вариант может быть сведён к варианту PMCP1.

Замечание 1.2. В постановке задачи PMCP значению параметра соответ­ ствуют экземпляров процесса. Существуют примеры систем, для которых 1 В дальнейшем переменные наблюдаемых процессов называются наблюдаемыми переменными.

модели с числом процессов меньше определённого не имеют смысла. В этом случае первые 1 процессов могут быть добавлены к процессу.

Замечание 1.3. В постановке задачи PMCP используется лишь один фиксиро­ ванный процесс и экземпляров прототипа процесса. Можно рассматри­ вать вариант задачи, в котором присутствуют несколько фиксированных про­ цессов 1,... и несколько прототипов процессов,,...,, а модель В некоторых случаях, когда устройство моделей параметризованного семей­ ства описывается с помощью сетевых грамматик, эта задача также сводится к постановке задачи PMCP с помощью построения LTS процесса в виде параллельной композиции LTS процессов 1,..., а LTS прототипа в виде параллельной композиции LTS прототипов,....

Методы и алгоритмы, представленные в работе, посвящённой верифи­ кации параметризованных моделей распределённых систем, опираются на существующие средства решения задачи MCP для конечных моделей. Для задачи MCP разработаны эффективные алгоритмы её решения, полиноми­ альные относительно числа состояний модели и полиномиальные или экспо­ ненциальные относительно размера формулы (в зависимости от логики). В данной работе не рассматриваются вопросы решения задачи MCP, они де­ тально описаны описаны во многих книгах, например, в [79, 102].

В данной главе приводится обзор работ, в которых предлагаются методы решения задачи PMCP.

В общем случае задача PMCP алгоритмически неразрешима [1], так как с помощью бесконечного семейства моделей моделируется задача останова машины Тьюринга. Простое доказательство данного факта приведено в ра­ боте [20] для случая однонаправленных колец. Однако существуют классы параметризованных моделей, для которых задача PMCP может быть реше­ на.

В обзоре методов решения задачи PMCP основное внимание уделяется следующим критериям:

Область применимости. Из неразрешимости задачи PMCP следует, что универсального метода решения задачи быть не может. Поэтому каж­ дому методу присущи ограничения на параметризованные модели, к которым применим метод. Важными ограничениями являются следую­ Топология. Описание видов топологий, к которым применим метод.

Вид параллелизма. Синхронный и/или асинхронный.

Способы взаимодействия процессов. Взаимодействие с помощью общих переменных, синхронного обмена сообщениями, асинхрон­ ного обмена сообщениями, широковещательного обмена сообщени­ ями. Как показано в работе [22], с точки зрения разрешимости задачи PMCP коммуникационные примитивы имеют разную вы­ Ограничения на структуру LTS процессов. Накладываются ли дополнительные ограничения на множества состояний и систему переходов процессов. Примеры возможных ограничений: процессы могут передавать сообщение лишь одного типа, условие срабаты­ вания каждого перехода обязательно включает проверку значений определённых переменных всех процессов.©Igor V. Konnov, PhD Thesis, Вид проверяемых спецификаций. В методах могут использовать­ Степень алгоритмизации. Участие экспертов в работе метода. Требуются ли подсказки от пользователя.

Завершаемость. Есть ли гарантия завершаемости метода. Не для всех под­ ходов известны условия завершаемости, в некоторых случаях использу­ ются полуразрешающие процедуры.

Первые работы, посвящённые задаче PMCP, появились во второй поло­ вине 80-ых годов. За прошедшие тридцать лет показана разрешимость задачи для асинхронных однонаправленных колец с маркером одного типа [20], ко­ лец с произвольным типом маркера и дополнительными ограничениями на LTS процесса [23, 93], симметричных систем с глобальными предусловиями переходов [21, 24], широковещательных синхронных систем [21, 22, 61], систем с произвольной топологией и одним маркером [95]. Предложены различные полуразрешающие процедуры: подходы, основанные на поиске процесса-инва­ рианта [9–11, 52, 55, 64, 86, 97]; подходы, основанные на проверке достижимых состояний регулярных моделей1 [2, 30, 59, 88]; символьные методы верифи­ 1 Регулярными моделями моделями называют такие параметризованные семейства моделей, в ко­ торых объединение отношений переходов моделей семейства задаётся с помощью конечного автомата кации [4, 80, 85]. Указаны способы абстракции [2, 36, 47, 50, 57, 61, 95] для определённых классов систем.©Igor V. Konnov, PhD Thesis, Как правило, в методах решения задачи PMCP используются специфика­

LTL CTL

выделенных (наблюдаемых) процессов или глобальных переменных; индек­

LTL CTL

подформулы () являются формулами соответствующей темпоральной ло­ гики с одной свободной переменной и пропозициональными переменными процесса с номером ; формулы безопасности (живучести) над переменными всех процессов вида ( ), которые должны выполняться во всех (в каком­ либо) состояниях модели, достижимых из начального.©Igor V. Konnov, PhD Thesis, Исторически методы решения задачи PMCP развивались в следующих направлениях:

аналитические методы редукции;

методы абстракции;

символьные методы;

методы, основанные на поиске инварианта.

В аналитических методах редукции, как правило, указывается способ отображения моделей семейства параметризованных моделей на одну модель этого семейства (cut-off model). В этом случае точно известны ограничения, которым должны удовлетворять модели семейства.

Для методов абстракции также часто указывается способ отображения параметризованных моделей на одну модель, но эта модель не принадлежит (регулярного выражения) над алфавитом из множеств состояний процессов.

самому параметризованному семейству, а моделирует поведение любого чис­ ла однотипных процессов. Из способа отображения следуют структурные ограничения на параметризованные семейства моделей, которые могут быть верифицированы таким способом.

Символьные методы обычно используют модификации символьного под­ хода к решению задачи MC. Для описания параметризованного семейства мо­ делей используются системы переходов, в которых переходы задаются неяв­ но, с помощью символьных описаний. Например, множества переходов могут представляться регулярными выражениями или логическими формулами с кванторами существования и всеобщности. Для заданной системы переходов ищется множество состояний, достижимых из начальных состояний. В случае символьных методов, как правило, нет гарантии завершаемости.

В методах, основанных на поиске инварианта, ищется или конструиру­ ется процесс-инвариант, моделирующий поведение нескольких процессов си­ стемы. Инвариант должен обладать следующим свойством: система, состоя­ щая из инварианта с дополнительными однотипными процессами, также мо­ делируется инвариантом. С помощью индукции показывается, что система со сколь угодно большим числом однотипных процессов моделируется системой, состоящей из фиксированного числа процессов и инварианта. Основное отли­ чие от методов абстракции состоит в том, что не требуется явное отображе­ ние каждой модели параметризованного семейства на модель-инвариант.©Igor V. Konnov, PhD Thesis, Рассмотрим методы подробнее с точки зрения сформулированных кри­ териев сравнения. Далее под параметризованным семейством понимается бесконечное множество моделей = { }, где каждая модель = · · · состоит из фиксированного процесса и изоморфных процессов. Обозначим с помощью записи параллельную композицию процессов типа, т.е. = · · ·. Множество состояний процесса обозначается с помощью записи.

2.1. Аналитические методы редукции В аналитических методах редукции выбираются ограничения на струк­ туру LTS проверяемых параметризованных моделей. После этого выбирается некоторое отношение эквивалентности на системах переходов, обладаю­ щее свойством консервативности относительно заданного класса специфика­ ций :

После выбора отношения доказывается, что для любого семейства, структура LTS процессов которого удовлетворяют выбранным ограничениям, найдётся такое число, начиная с которого верно + для всех на­ туральных. В этом случае достаточно проверить спецификацию на моделях 1,...,. Модель называется пороговой моделью (cut-off), а число — пороговым значением.

Первая работа, в которой использовался такой подход, принадлежит Эмерсону (Emerson) и Намиоши (Namjoshi) [20]. В этой работе рассматрива­ ется класс асинхронных систем с топологией однонаправленного кольца, взаи­ модействующих с помощью синхронного обмена сообщениями. В LTS процес­ са допускаются только локальные переходы и синхронная передача маркера одного типа. В качестве отношения эквивалентности использовалось отноше­ ние блочной бисимуляции, предложенное авторами. Для спецификаций вида () являются формулами логики CTL -X относительно переменных процесса, аналитически построено отношение блочной симуляции и найдены порого­ вые значения = 2, 3, 4, 5 соответственно.

В работе Эмерсона (Emerson) и Калон (Kahlon) [23] рассматриваются так же асинхронные системы с топологией двунаправленного кольца процес­ сы, обменивающиеся типизированным маркером в однонаправленном кольце.

При этом каждый процесс может изменять тип маркера ограниченное чис­ ло раз (число ). Для этого случая и спецификаций в виде формул логики указывается пороговое значение (), зависящее от систем переходов LTL-X процессов. В той же работе показана алгоритмическая разрешимость задачи PMCP для двунаправленных колец с маркером.

В работе [21] Эмерсон и Калон рассмотрели класс асинхронных парамет­ ризованных систем с широковещательным обменом сообщениями. При этом условия LTS процессов должны иметь специальный вид: условие перехода является либо дизъюнкцией ( · · · ) по состояниям,..., всех про­ цессов, отличных от активного (guarded broadcast); либо конъюнкцией () по начальным состояниям всех процессов, отличных от активного (initialized broadcast). Также процесс всегда может перейти в начальное состояние. Для таких параметризованных моделей указано пороговое значение = 7 при гики относительно переменных процессов и. Подробное изложение результатов приведено в работе [49]. Среди систем, удовлетворяющих указан­ ным ограничениям, известны модели протоколов когерентности кэшей мно­ гопроцессорных систем.

Достоинства. Несомненными достоинствами аналитических методов ре­ дукции являются: точное описание области применимости методов, алгорит­ мизация и завершаемость. С помощью средств MC достаточно проверить все модели 1,..., до порогового значения, где известно заранее.

Недостатки. Среди недостатков подхода можно перечислить следующие.

Во-первых, аналитические методы редукции применимы только к двум видам систем: асинхронным системам с кольцевой топологией, процессы которых об­ мениваются маркером, а также асинхронным широковещательным системам с переходами специального вида. Во-вторых, теоретические оценки порогово­ го значения для некоторых методов зависят от числа состояний процессов, поэтому число состояний пороговой модели может быть настолько большим, что в результате проверка пороговой модели будет практически невозмож­ ной.©Igor V. Konnov, PhD Thesis, 2.2. Методы абстракции Идею методов абстракции можно описать следующим образом. Для па­ раметризованных семейств и каждого натурального числа задаётся отоб­ ражение модели на абстрактную модель. После чего проверяется мо­ дель с фиксированным числом процессов, одним процессом и одним процессом. Выбор числа, вида модели и отображения зависит от метода. В некоторых методах число равно 0. Стоит сразу заметить, что вид модели и отображения определяется экспертом.

Одной из первых работ, в которой использовался такой подход, является работа Германа (German) и Систлы (Sistla) [28]. В этой работе рассматрива­ ется класс систем асинхронно-взаимодействующих процессов с топологией «звезда». В центре находится управляющий процесс, с которым соеди­ нено изоморфных клиентских процессов. Абстрактная модель стро­ ится в виде графа VASS (Vector Addition State System). Пусть множество = {1,..., } — множество состояний процесса, упорядоченное произ­ вольным способом. В LTS каждый процесс находится в одном из состоя­ ний из множества. Вершинами графа являются кортежи (1,..., ).

Эти вершины соответствуют состояниям LTS для различных значений, в которых для любого, 1, число процессов, находящихся в со­ стоянии, равно. Число вершин в получившемся графе бесконечно, но авторы показывают, что для проверки свойств достаточно ограничиться про­ смотром конечных путей из вершины, соответствующей начальному состоя­ нию. Таким образом, метод гарантированно завершается. Однако сложность просмотра дважды экспоненциальна относительно числа состояний клиент­ ских процессов, поэтому на практике метод может оказаться неприменимым.

Спецификации задаются с помощью формул для одного наблюдаемого процесса.

В работе Айпи (Ip) и Дилла (Dill) [47] для построения абстрактной моде­ ли асинхронной системы применяется похожая идея. Однако вместо полно­ го графа VASS используется его абстракция: в вершинах (1,..., ) графа, соответствующего модели, элементы принимают значения из множества {0, 1, +}. Элементы 0, 1, + соответствуют числу процессов 0, 1 и более од­ ного. Таким образом, любая модель семейства отображается на модель с конечным числом состояний, в любом состоянии которой хранятся абстрак­ ции числа процессов для каждого исходного состояния процесса. С помо­ щью указанного отображения абстракции успешно проверялись параметри­ зованные модели протоколов когерентности кэшей (MESI, ICCP и DCCP) в системе верификации моделей Mur. Метод всегда завершается, но специфи­ кация может не выполняться на абстрактной модели. В таком случае нель­ зя сделать вывод о выполнимости спецификации на моделях семейства.

Спецификации задаются с помощью формул логики ACTL над глобальными переменными системы.©Igor V. Konnov, PhD Thesis, Модификация графа VASS используется для проверки асинхронных си­ стем с разделяемыми переменными и в работе Лесена (Lesens) и Сайди (Saidi) [57]. По описаниям процессов с помощью САДТ PVS [73] проводится булева абстракция систем переходов и неявно строится абстрактная модель, система переходов которой представлена системой линейных ограничений.

Для системы линейных ограничений с помощью стандартных средств ищется решение системы, в котором более одного процесса находится в заданном состоянии. Состояние соответствует критической секции. Если решение найдено, то в критической секции находится более одного процесса и свойство взаимного исключения процессов в критической секции наруша­ ется. Ключевым моментом метода является построение булевой абстракции графа с помощью САДТ. При построении абстракции пользователь должен указать предикаты над переменными системы переходов, используемые при абстракции. Авторы продемонстрировали применимость метода для алгорит­ мов взаимного исключения в критической секции.

В работе Кларка (Clarke) и др. [95] рассматриваются параметризованные модели распределённых систем с асинхронным параллелизмом и произволь­ ной топологией, в которых процессы обмениваются одним маркером. Для процессов указывается способ построения абстрактной LTS и отображе­ ние LTS на LTS. После чего доказывается, что для проверки формулы выполнимости логики на семействе достаточно проверить выпол­ нимость формулы на LTS. Алгоритм построения абстрактной модели всегда завершается.

Дженсен (Jensen) и Линч (Lynch) [48] исследовали параметризованную модель протокола Бёрна, использующегося для взаимного исключения про­ цессов в критической секции. Для LTS процессов этого протокола Дженсен и Линч указывают абстрактную модель = 2 и отображение модели на модель. Абстрактная модель и отображение строились авторами вручную. Проверка корректности отображения проводилась с использова­ нием САДТ. Проверка свойства критической секции на модели, заданного в виде формулы логики осуществлялась с помощью верификатора моде­ лей Калдер (Calder) и Миллер (Miller) в работе [7] проверили модель сорев­ нования процессов в протоколе Firewire. Для этого авторы применили способ построения абстрактной модели, аналогичный описанному выше приме­ нительно к работе Айпи и Дилла [47]. Авторы рассматривали специальный класс моделей, в которых каждое вычисление ведёт в финальное состояние.

Такие модели авторы назвали деградирующими (degenerating). Абстракция применялась авторами и для проверки моделей телекоммуникационных про­ токолов [8].

Достоинства. Основное достоинство методов абстракции заключается в том, что после нахождения вида абстрактной модели и отображения моделей семейства на абстрактную модель, проверка свойств осуществляется ав­ томатически для любой параметризованной модели (за исключением метода Лесена и Сайди, где булева абстракция строится с помощью САДТ).

Методы верификации параметризованных моделей с помощью абстрак­ ции опираются на постоянно развивающийся аппарат построения булевых абстракций и абстрактной интерпретации. Поэтому область применимости методов абстракции к задаче PMC постепенно расширяется.©Igor V. Konnov, PhD Thesis, Недостатки. Даже в тех случаях, когда экспертам удаётся указать вид абстрактной модели и способ абстракции для класса моделей, область применимости методов ограничивается: системами, процессы которых обме­ ниваются маркером [95]; широковещательными системами [47]; системами с топологией «звезда» [28]. В остальных случаях методы абстракции требуют подсказок от эксперта. Например, требуется явное указание существенных переменных и предикатов в системах переходов.

Более того, когда абстракция построена, спецификация может не вы­ полняться на абстрактной модели. Из чего не следует, что спецификация нарушается и на моделях параметризованного семейства. В таком случае требуется участие эксперта для уточнения абстракции, однако уточнение воз­ можно не для всех указанных методов.

2.3. Символьные методы Символьные методы решения задачи PMCP берут начало от символьных методов решения задачи MCP. Идея символьных методов MC заключается в представлении отношения переходов LTS в виде формул логики высказы­ ваний. Операции поиска достижимых состояний, используемые в MC, заме­ няются операциями логического вывода. Часто формулы логики высказыва­ ний представляются с помощью двоичных разрешающих диаграмм (Binary Decision Diagrams, BDD [19]).

В случае задачи PMCP формул логики высказываний оказывается недо­ статочно для применения символьных методов. По этой причине для описа­ ния систем переходов используются другие языки: регулярные выражения, арифметика Пресбургера, логики с квантором по одной переменной и т.п. С помощью выбранного языка сразу для всех моделей семейства описывают­ ся: множество начальных состояний моделей семейства ; преобразователь множества состояний системы, соответствующий отношению переходов;

спецификация, которая должна выполняться на множестве достижимых состояний.

В символьных методах задача PMC сводится к проверке достижимости состояния, в котором нарушается спецификация, из множества начальных состояний с помощью переходов, заданных преобразователем. Символь­ ные методы решения задачи PMCP использовались, в основном, для про­ верки алгоритмов взаимного исключения процессов в критической секции.

Чаще всего рассматриваются системы с асинхронным параллелизмом, в ко­ торых процессы взаимодействуют посредством разделяемых переменных. То­ пология коммуникационной сети, как правило, соответствует полносвязному графу.©Igor V. Konnov, PhD Thesis, В работах [30, 37, 71, 88] преобразователь задаётся в виде регулярного выражения над алфавитом. По преобразователю итеративно строится его транзитивное замыкание +, соответствующее транзитивному замыка­ нию отношения переходов. После чего проверяется пустота пересечения язы­ ков ¬ и (). Если пересечение языков пусто, то спецификация верна в состояниях, достижимых из множества, заданного описанием. Данный под­ ход получил название «Верификация регулярных моделей» (Regular Model Checking). При применении метода возникает несколько проблем. Итератив­ ное вычисление + не обладает свойством завершаемости, так как преобра­ зователь не ограничен сверху. Поэтому часто строится аппроксимация транзитивного замыкания + с помощью подсказок эксперта. Как и в случае методов абстракции из нарушения спецификации на множестве состояний, вычисленных с помощью аппроксимации, не следует нарушение специфи­ кации на множестве достижимых состояний.

Похожий подход используется и в работе Кестена (Kesten) и др. [89].

Помимо регулярных выражений над алфавитом используются автоматы над деревьями, в вершинах которых находятся состояния процесса. Ана­ логично для древовидной топологии вычисляется аппроксимация множества достижимых состояний. Данный подход подробно изложен в работе Шаха­ ра (Shahar) [85], там же предложены способы проверки не только свойств безопасности, но и живучести.

В работе Хенриксена (Henriksen) и др. [69] для представления преобразо­ вателя используется одноместная логика второго порядка (Monadic Second Order Logic, M2L). Описания на языке M2L транслируются в BDD и прове­ ряются с помощью средства Работа Майдл (Maidl) [61] посвящена проверке параметризованных мо­ делей, в которых преобразователь описан с помощью арифметики Пресбур­ гера. Процессы взаимодействуют с помощью разделяемой памяти или широ­ ковещательной рассылки сообщений. Проверяемые спецификации задаются с помощью формул линейной логики относительно переменных однотипных процессов. Показано, что с помощью используемого представления и алгорит­ мов проверки формул арифметики Пресбургера задача PMC разрешима для систем с кольцевой топологией и широковещательных систем. Полученные результаты о разрешимости задачи PMC схожи с результатами работ [21, 22].

Достоинства. Символьные методы могут применяться для проверки свойств безопасности параметризованных моделей асинхронных распределён­ ных систем со следующими топологиями: кольцевая, древовидная, полносвяз­ ная. Положительным свойством методов является использование хорошо из­ вестных в математической логике языков и готовых средств вывода для этих языков. Выразительные возможности применяемых языков позволяют опи­ сывать протоколы, параметризованные не только по числу процессов, но и использующие бесконечные типы данных, например, целочисленные счётчи­ ки.

Недостатки. Так как символьные методы основаны на представлении си­ стем переходов параметризованного семейства в целом с помощью более выразительных языков, нежели LTS, размеченных пропозициональными пе­ ременными, завершаемость методов, в общем случае не гарантируется. В некоторых случаях завершаемость может быть достигнута модификацией преобразователя, например, с помощью применения техник добавления до­ полнительных переходов (акселерация, acceleration) и поиска аппроксимаций (расширение, widening). Однако в этом случае требуется участие эксперта с целью изменения преобразователя.

Другим недостатком, существенным с точки зрения целей настоящей ра­ боты, является требование повторного описания модели в параметризованном виде на языках, сильно отличающихся от языков описания моделей, исполь­ зуемых в средствах MC. После того, как модель распределённой системы по­ строена и верифицирована для фиксированного числа процессов с помощью стандартного средства MC, желательно использовать выбранный уровень аб­ стракции и перевести модель в параметризованный вид с минимальным вме­ шательством эксперта.©Igor V. Konnov, PhD Thesis, 2.4. Методы, основанные на поиске инварианта Первый метод, использовавшийся для решения задачи PMC, основан на поиске LTS, называемой инвариантом, для параметризованного семейства и индуктивном доказательстве о сводимости задачи верификации специфи­ кации на всех моделях семейства к задаче верификации модели, содержащей процессы моделей параметризованного семейства и инвариант. Далее все ме­ тоды, основанные на поиске инварианта, называются кратко методами инва­ риантов. Обзор методов инвариантов приведён в работе [6].

В работах [9, 52, 97] заложена основа методов инвариантов, идея кото­ рого заключается в следующем. На множестве LTS выбирается отношение эквивалентности или частичного порядка. Выбранное отношение порядка должно быть монотонным относительно операции параллельной компо­ зиции, т.е. для любых LTS { }4 из соотношений 1 2 и должно следовать соотношение 1 3 2 4. Отношение так­ же должно удовлетворять свойству консервативности для заданного класса спецификаций, т.е. для любых LTS 1 и 2 и любой формулы из соотношений 1 2 и 2 |= следует соотношение 1 |=.

Для заданного семейства ищется LTS, называемая инвариантом, удовлетворяющая свойствам: и. После чего индукцией по числу процессов с помощью свойства монотонности показывается, что.

Из свойства консервативности следует, что спецификацию достаточно проверить на модели. Если спецификация выполняется на модели, то она выполняется и на всех моделях, 1, семейства.

В работе Кларка (Clarke), Грамберг (Grumberg) и Брауна (Browne) [9] в качестве отношения используется отношение эквивалентности, называе­ мое авторами отношением соответствия. В следующей работе авторов [3] на основании этого отношения определено отношение прореженной эквивалент­ ности или прореженной бисимуляции (stuttering bisimulation). Спецификации задаются с помощью формул индексированной логики т.е. формул вида (), в которых подформулы () являются эквивалентными форму­ лами логики с одной свободной переменной, а все пропозициональ­ ные переменные () являются переменными процесса с номером. В работе вручную конструируется отношение соответствия для алгоритма взаимного исключения в критической секции с топологией кольца. В качестве инвари­ анта используется процесс =.©Igor V. Konnov, PhD Thesis, Куршан (Kurshan) и МакМиллан (McMillan) явно формулируют теорему об индукции в методе инвариантов [52]. Отношение задаётся как отношение языкового включения трасс процессов. Процессы объединяются в линейную топологию с помощью синхронной параллельной композиции. Предлагаемый подход работает автоматически. В качестве инварианта используется процесс Вольпер (Wolper) и Лёвинфосс (Lovinfosse) описали [97] метод инвариан­ тов для случая =. Процессы объединяются в линейную или кольцевую топологию с помощью асинхронной параллельной композиции. В качестве отношения используется отношение трассового включения с наблюдением отказов и дивергенции («зацикливания») процессов. В примерах инвариант строится вручную.

До появления работы Штадлера (Shtadler) и Грамберг (Grumberg) [86] решения задачи PMC предлагались для двух простых топологий распреде­ лённых систем: линейной и кольцевой. В работе [86] топология параметризо­ ванного семейства описывается с помощью сетевых (графовых) грамматик.

Терминалами сетевой грамматики являются LTS, в правилах вывода задают­ ся способы порождения экземпляров процессов и их синхронизации. Каждо­ му слову грамматики соответствует модель из семейства. Для описания дексированной логике Процессы взаимодействуют с помощью обме­ на сообщениями, композиция процессов асинхронная. Для проверки свойства строятся абстрактные графы коммуникационного поведения LTS (communication behaviour), которые проверяются на изоморфность.

Подход, описанный в работе [86], развивается в работе Марелли (Marelly) и Грамберг [64] и далее в работах Кларка, Грамберг и Джа (Jha) [10, 11]. В работе [10] в качестве отношения уже используется отношение строгой си­ муляции. Для процессов, участвующих в правилах вывода, строятся абстракт­ ные LTS, в которых используются регулярные выражения над состояниями процессов. В модели применяется синхронный параллелизм. В работе [11] результаты так же применяются для асинхронного параллелизма с исполь­ зованием отношения строгой симуляции, однако это отношение на практике применимо в методе только в случае довольно сильной абстракции.

В работе Лесенса (Lesens), Гальбаха (Galbwachs) и Раймонда (Raymond) [55] рассматриваются параметризованные модели с линей­ ной и древовидной топологиями и синхронным параллелизмом. Отношение является отношением трассового включения. Проверяемые специфи­ кации выражаются с помощью дополнительных процессов, называемых наблюдателями (observers). Инвариант ищется автоматически. Для этого вводится монотонный оператор добавления дополнительных процессов, действующий на множествах трасс. Для оператора строится неподвижная точка. Оператор неограниченный, поэтому процедура поиска, в общем случае, может не завершиться. Как и в символьных методах, эксперт может модифицировать системы переходов, применяя техники акселерации и расширения.

Кестен (Kesten) и Пнуели (Pnueli) применяют [50] комбинацию методов абстракции и инвариантов. Отношение определяется как отношение мо­ дульной абстракции, сочетающее построение абстрактного графа поведения и трассового включения. С помощью отношения модульной абстракции ищет­ ся инвариант. Применимость метода демонстрируется на примерах алгоритма взаимного исключения и обедающих философов, инварианты для которых строятся вручную. Важным достижением работы является сочетание мето­ дов инвариантов и абстракции, в том числе, для процессов с целочисленными счётчиками.©Igor V. Konnov, PhD Thesis, Калдер (Calder) и Миллер (Miller) в работе [7] использовали индукцию и отношение прореженной бисимуляции для проверки модели соревнования процессов в протоколе Firewire. Фактически, обоснование корректности ре­ дукции проводилось вручную.

Достоинства. В методах инвариантов используется способ индуктивного доказательства и довольно простой критерий проверки инварианта. Поэто­ му методы могут быть автоматизированы. Поиск инварианта среди моделей семейства с малым числом процессов соответствует интуитивному пред­ ставлению инженеров, разрабатывающих модель, о поведении модели.

С помощью методов инвариантов могут проверяться параметризованные модели с нетривиальной топологией, представляемой сетевыми грамматика­ ми, и различными прототипами процессов.

Существенным достоинством является и то, что после нахождения ин­ варианта (или нескольких инвариантов в случае сетевой грамматики), для проверки модели, содержащей инвариант, достаточно применить развитые средства метода верификации моделей.

Недостатки. В тех случаях, когда не удаётся найти инвариант среди моде­ лей с малым числом процессов, необходимо дополнительно применять методы абстракции, требующие знаний эксперта.

Так как автоматический поиск инварианта проводится среди моделей семейства, в общем случае для процедуры поиска нет гарантии завершаемо­ сти. Однако, на практике инварианты необходимо искать среди моделей с довольно небольшим числом процессов, так как размер множеств состояний в моделях параметризованного семейства растёт экспоненциально с числом процессов.©Igor V. Konnov, PhD Thesis, 2.5. Выводы, выбор метода и декомпозиция задачи Как следует из описания достоинств и недостатков представленных мето­ дов решения задачи PMCP, большинство аналитических методов редукции и методов абстракции обладает свойствами алгоритмизации и завершаемости.

Однако область применимости обеих групп методов невелика: асинхронные модели, в которых процессы обмениваются маркером; асинхронные модели с широковещательной передачей сообщений; асинхронные модели с топологией «звезда». При необходимости проверки моделей с другой топологией требу­ ется разработка новых методов, возможно, аналогичных уже известным.

Сравним символьные методы и методы инвариантов. Символьные ме­ тоды и методы инвариантов применяются к параметризованным моделям с различной топологией: кольцевой, линейной, древовидной. Символьные мето­ ды применяются, в основном, для проверки свойств безопасности, в то время как многие методы инвариантов применимы и для проверки свойств живуче­ сти. Обе группы методов используют полуразрешающие процедуры, поэтому, в общем случае, не завершаются.

Для применения символьных методов описание параметризованной мо­ дели требуется представить на специальном языке метода, обычно доволь­ но сильно отличающегося от языков описания моделей средств MC. Методы инвариантов используют описания процессов в виде LTS, размеченных про­ позициональными переменными, и совместимы с языками описания моделей средств MC. Методы инвариантов используют для проверки спецификации и поиска контрпримеров существующие средства MC, символьные же методы требуют реализации специальных алгоритмов.©Igor V. Konnov, PhD Thesis, Учитывая вышесказанное, в настоящей работе в качестве базового мето­ да выбран метод инвариантов, а процедура порождения моделей параметри­ зованного семейства и поиска инвариантов основана на процедуре, использу­ емой в методах сетевых инвариантов [10, 11, 64, 86].

В работе [10] при поиске инвариантов моделей с синхронным паралле­ лизмом в качестве отношения используется отношение строгой симуляции, обладающее необходимыми отношениями консервативности и монотонности.

В следующей работе [11] это же отношение используется и для поиска инва­ риантов моделей с асинхронным параллелизмом. Однако отношение строгой симуляции требует соответствия поведения моделей, характерного для моде­ лей с синхронным параллелизмом.

Как и в случае отношений эквивалентности моделей, отличающихся для моделей с синхронным и асинхронным параллелизмом [94], в качестве же­ лательно использовать отношение, схожее с отношением симуляции, но при этом не различающее внутренних, ненаблюдаемых событий процессов. При этом, чем слабее такое отношение, тем потенциально большее множество мо­ делей находится в таком отношении и тем больше шансов на успешный поиск сетевого инварианта. Сложность алгоритма построения отношения также яв­ ляется одним из главных факторов при поиске нужного отношения.

Декомпозиция задачи 1. Поиск ослабленных отношений симуляции на LTS, обладающих необхо­ димыми свойствами для применения метода сетевых инвариантов с це­ лью проверки асинхронных параметризованных моделей распределён­ ных систем.©Igor V. Konnov, PhD Thesis, 2. Разработка алгоритмов построения найденных ослабленных отношений симуляции. Доказательство корректности и оценка сложности разрабо­ танных алгоритмов.

В данной главе приводятся основные определения, используемые при описании параметризованных моделей распределённых систем и специфика­ ций свойств моделей. Основой настоящих определений являются определе­ ния, используемые в работах [10, 20, 102].

3.1. Размеченные системы переходов Пусть задано множество (может быть, бесконечное) всевозможных меток действий A. Действия соответствуют классам эквивалентности событий DS.

Примерами действий служат: присваивание значения переменной процесса, посылка сообщения процессом, приём сообщения процессом. Далее, подра­ зумевается, что действия всех размеченных систем переходов находятся в множестве A. В множестве A также находится специальное ненаблюдаемое действие.

Определение 3.1. Размеченной системой переходов (Labelled Transition System, LTS) называется шестерка (, 0,,,, ), в которой — конечное множество состояний, 0 — подмножество начальных состояний системы, A — конечное множество меток действий (в дальнейшем, просто дей­ ствий), — отношение переходов на множестве, — конечное множество булевых переменных системы, — функция разметки состояний В дальнейшем мы будем использовать запись, означающую (,, ) для,,. С помощью отношения задаются возмож­ ные варианты дискретных переходов из одного состояния в другое. Переходы сопровождаются метками действий.

Для каждого состояния с помощью функции задаются значения булевых переменных из множества в состоянии. Если для переменной верно (), то переменная принимает значение «истина» в состоянии PhD Thesis, С помощью символа M мы будем обозначать множество всех размечен­ ных систем переходов.

Определение 3.2. Конечным путём в размеченной системе переходов (, 0,,,, ) называется такая конечная последовательность чередую­ ным путем называется такая бесконечная последовательность чередующихся чаться с помощью записи 1 2... 1, а бесконечный путь = Для конечного или бесконечного пути запись (, ) означает суффикс пути, начинающийся из состояния.

Определение 3.3. Для путей на множестве состояний введём функцию состояний, встречающихся на пути, : * 2. Состояние когда найдётся такое 1, что =.©Igor V. Konnov, PhD Thesis, Определение 3.4. Пусть дана система переходов = (, 0,,,, ).

= 1. Конкатенацией путей и назовём путь = 1... Далее для обозначения конкатенации путей и используется запись Обычно в множество действий добавляется действие, означающее нена­ блюдаемое действие. Действие играет особую роль при построении па­ раллельной композиции моделей: переход, соответствующий взаимодействию двух процессов, размечается ненаблюдаемым действием.

Определение 3.5. Для системы переходов, 0,,,, состояние называется достижимым из состояния, если найдётся некоторый ко­ нечный путь = 1.... Состояние называется достижимым, если оно достижимо из некоторого начального состояния системы перехо­ дов.©Igor V. Konnov, PhD Thesis, Пример 3.1 (Пример размеченной системы переходов). В качестве примера размеченной системы переходов рассмотрим древовидный волновой алгоритм (tree wave algorithm) [91, гл.7]. Волновые алгоритмы используются в качестве базы для создания более сложных алгоритмов: обнаружения завершения, вза­ имного исключения. В древовидном волновом алгоритме участвуют процессы трёх типов: корневой процесс-инициатор (прототип Root); процесс, соответ­ ствующий листовой вершине коммуникационного дерева (прототип Inner);

процесс, соответствующий внутренней вершине коммуникационного дерева (прототип Leaf).

В алгоритме процесс-инициатор (корневой процесс типа Root) посылает сообщение своим потомкам. Процессы типа Inner получают сообщение от ро­ Рисунок 3.1. Диграммы LTS процессов типа Root, Inner, Leaf дительского процесса и посылают его своим потомкам. Процессы типа Leaf получают сообщение, запускают задачу принятия решения (в данном случае задача принятия решения не интересна) и посылают обратно подтверждение (в данном примере используется один тип сообщений). Процессы типа Inner, получив подтверждение, от всех потомков также запускают задачу принятия решения, после чего передают подтверждение родителю.©Igor V. Konnov, PhD Thesis, На рисунке 3.1 изображены диаграммы LTS прототипов процессов древо­ видного волнового алгоритма для бинарного дерева. Состояния LTS изобра­ жаются эллипсами. Начальные состояния: 0, 0 и 0. Переходы помечаются действиями _, _, _, _. Действия с префик­ сом соответствуют приёму сообщения, а действия с префиксом со­ ответствуют посылке сообщения. Переходы, для которых не указана метка, помечены действием.

Определим функцию переименования действий на LTS. Пусть задана LTS =. Тогда результатом применения функции к LTS (обозначе­ (, (), ).©Igor V. Konnov, PhD Thesis, В дальнейшем мы будем использовать специальную функцию при­ писывания индекса действиям LTS, отображающую каждое действие на действие.

3.2. Асинхронная параллельная композиция В примере 3.1 в LTS процессов используются действия с префиксами и, соответствующие посылке и получению сообщений. Для описания пра­ вил взаимодействия на размеченных системах переходов вводится операция параллельной композиции. При помощи операции параллельной композиции строится новая LTS, моделирующая асинхронное выполнение и синхронный обмен сообщениями двух исходных LTS. Имея LTS всех процессов модели­ руемой DS можно построить LTS всей DS, применяя итеративно операцию параллельной композиции.

Определение 3.6. Пусть заданы такие LTS 1 = (1, 1, 1, 1, 1, 1 ) и Тогда модель = (, 0,,,, ) называется (асинхронной) параллельной композицией систем 1 и 2, если:

Отношение переходов (1 2 )(1 2 ) задаётся следующим образом: ((, ),, (, )) тогда и только тогда, когда выполняется 3. выполняется синхронный обмен сообщениями: (,, ) 1, Пример 3.2 (Пример композиции). Пусть 1, 2 — LTS двух процессов, по­ лученных из LTS прототипов Inner и Leaf соответственно путём переимено­ вания с помощью функций и. Зададим синхронизатор = (, ) следующим образом: = {_ 1, _ 1 }, _ 1 = _2, Примерами переходов LTS = 1 2 служат следующие переходы:

внутренний переход первого процесса (0, 0 ) (1, 1 ), внутренний переход второго процесса (7, 8 ) (7, 0 ), коммуникационный переход обоих процессов (1, 0 ) (2, 1 ).

3.3. Описание топологии распределённых систем с помощью сетевых грамматик Для описания топологии параметризованной распределённой системы как и в работах [10, 86] используются сетевые грамматики.

Определение 3.7. Контекстно-свободной сетевой грамматикой называется такая четвёрка = (,,, ), в которой:

множество — множество терминалов, процессов в виде LTS;

множество — множество нетерминалов;

символ — стартовый символ, множество — множество правил вывода вида: 1 [1 ] · · · 1 [ ], в каждом из которых участвуют:

– функции переименования действий : A A.

Далее предполагается, что грамматика однозначна, не содержит беспо­ лезных и недостижимых символов, а также содержит только циклы вида

1 · · ·, где и 1,...,.©Igor V. Konnov, PhD Thesis,

С помощью сетевой грамматики порождаются LTS, соответствующие мо­ делям параметризованного семейства. Для порождения LTS по грамматике мы используем деревья вывода, совпадающие с деревьями вывода в обычных контекстно-свободных грамматиках. Для обозначения дерева вывода, состоя­ щего из одного терминала, используется запись. В случае применения правила 1 [1 ] 1 · · · 1 [ ] используется запись ( 1... ), где 1,..., — деревья вывода для символов 1,...,. Множество всех деревьев вывода из символа с терминальными листовыми вершинами обо­ значим с помощью записи (), а подмножество деревьев высоты из множества () — с помощью ().

Чтобы исключить коллизии имён переменных в LTS, порождаемых од­ ним терминалом, для натурального числа определим аналогично функ­ ции переименования действий функцию переименования переменных моде­ ли : M M. Для LTS =, 0,,,, и натурального числа результатом применения функции (обозначение [ ]) является LTS =,,,,,, обладающая следующими свойствами:

верно = { | }, т.е. к имени каждой переменной приписывается значение функции разметки : 2 для состояния равно определяется следующим образом:

если = ( 1... ) и соответствующее корню дерева правило вы­ Пример 3.3 (Пример сетевой грамматики). Рассмотрим пример сетевой грам­ матики для древовидного волнового алгоритма, описанного в примере 3.1.

Грамматика = ({, }, {,, },, ). Прототипы процессов Root, Inner и Leaf обозначаются символами,, соответственно.

Правила вывода задаются следующим образом:

Синхронизаторы 1 и 2 задаются аналогично синхронизатору в приме­ ре 3.2. Функции переименования задаются следующим образом. Для функ­ для остальных значений. Для функции 2 верно 2 (_) =, 2 (_) = и 2 () = для остальных значений. Для функ­ 3 (_) = и 3 () = для остальных значений.

С помощью сетевой грамматики порождаются модели параметризо­ ванного древовидного волнового алгоритма с различным числом процессов.

мы получим дерево вывода 3 = ( ( ) ( ) ). Применив функ­ цию к дереву 3, мы получим LTS с одним корневым и двумя листовыми процессами 3 = (3 ), принадлежащую параметризованному семейству.

3.4. Темпоральные логики Спецификацию поведения распределённых систем можно задавать раз­ личными способами. Одним из языков спецификаций являются темпораль­ ные логики. С помощью темпоральных логик описываются свойства, в кото­ рых используется временная связь между различными событиями.

Приведём кратко определения, которые могут быть найдены в [102, гл. 3], следующих логик: деревьев вычислений (CTL ), ветвящегося времени (CTL), линейного времени (LTL).

Синтаксис логики Пусть — множество булевых переменных.

формулы состояния и вспомогательные формулы пути.©Igor V. Konnov, PhD Thesis, Формулы состояния и пути определяются следующим образом:

если, то — формула состояния;

если и — формулы состояния, то,, ¬ — формулы состояния;

если — формула состояния, то — формула пути;

если и — формулы состояния, то X, F, G, U — формулы пути.

Формулами логики являются формулы состояния.

нимость формулы в состоянии LTS, а с помощью записи, |= — выполнимость формулы на пути LTS. Семантика формул логики CTL для LTS =, 0,,,, определяется следующими правилами:

Выражение, |= верно тогда и только тогда, когда ().

Выражение, |= ¬ верно тогда и только тогда, когда неверно, |= (обозначается, |= ).

Выражение, |= (, |= ) верно тогда и только тогда, когда верно, |= и (или), |=.

существует путь из состояния такой, что, |=.

Выражение, |= верно тогда и только тогда, когда для любого пути в из состояния верно, |=.

Выражение, |= верно тогда и только тогда, когда для первого состояния пути верно, |=.

Выражение, |= ¬ верно тогда и только тогда, когда неверно Выражение, |= (, |= ) верно тогда и только тогда, когда верно, |= и (или), |=.©Igor V. Konnov, PhD Thesis, Выражение, |= верно тогда и только тогда, когда существует Выражение, |= верно тогда и только тогда, когда для любого Выражение, |= U верно тогда и только тогда, когда существует Формула выполняется на LTS =, 0,,,,, если для любого начального состояния 0 0 верно, 0 |=. Выполнимость на LTS обозначается с помощью записи |=.

Формулы логик линейного и ветвящегося времени являются подмноже­

CTL CTL

формулах логики допускается только один квантор пути в самом начале формулы — квантор A. При записи формулы LTL квантор обычно опускается.

и соответственно, в формулах которых отсутствует темпоральный опе­ ратор X. Также используется подмножество ACTL логики CTL, в формулах ральный оператор X.

Часто свойства распределённых систем формулируются в виде свойств безопасности и живучести. Свойства безопасности описывают такие пути в модели, в которых состояния модели всегда находится в опредённом множе­ стве «безопасных состояний». Примером свойства безопасности может слу­ что один из двух процессов всегда находится вне критической секции. Свой­ ства живучести описывают такие пути в модели, в которых модель, рано или поздно, попадёт в «хорошее состояние». Примером такого свойства служит 3.5. Конечные и бесконечные блоки Так как в работе рассматриваются модели с асинхронной параллельной композицией в дальнейшем изложении для нас будут представлять интерес пути специального вида, называемые блоками [9, 20]. С точки зрения прове­ ряемых спецификаций некоторые переходы размеченной системы переходов могут быть важны для выполнимости спецификации, а некоторые — нет. По­ следние переходы можно считать ненаблюдаемыми. В конечных блоках все переходы, за исключением последнего, относятся к ненаблюдаемым. В бес­ конечных блоках все переходы не наблюдаются. В общем случае для LTS с отношением переходов множеством наблюдаемых переходов мы будем считать произвольное множество переходов.©Igor V. Konnov, PhD Thesis, В качестве множества наблюдаемых переходов можно взять, напри­ мер, множество переходов с действиями, отличными от, или изменяющими значения переменных из выделенного множества 0 :

Множество 0 может быть построено по проверяемой спецификации.

В этом случае в 0 включаются все пропозициональные переменные, встре­ чающиеся в формуле. Для произвольной формулы можно построить множество наблюдаемых переменных, используемых в формуле. Если (, ), наблюдаемых переходов называется согласованным относительно формулы.

Множество наблюдаемых переходов (, 0 ) относительно задан­ ного множества переменных 0 часто используется в дальнейших определе­ ниях. В тех случаях, когда из текста понятно, о какой модели и множестве переменных 0 идёт речь, используется запись вида для любого такого перехода, что (,, ) (, 0 ).

Для LTS =, 0,,,,, заданного регулярного языка и двух состояний, мы будем писать, если из состояния найдётся запись означает, что из состояния существует путь в состояние с переходами с действиями и заканчивающийся переходом с действием.

Обозначение переносится на множества состояний следующим образом: для двух множеств состояний и верно тогда и только тогда, когда найдутся такие состояния и, что.

Определение 3.8. Конечным блоком из состояния 1 относительно множе­ ства наблюдаемых переходов назовём такой конечный путь = всех : 1 <. Переход (,, +1 ) назовём финальным. Бесконечным блоком из состояния 1 относительно множества наблюдаемых переходов назовём такой бесконечный путь = 1 2 · · · · · ·, что (,, +1 ) выполняется для всех 1.©Igor

/ V. Konnov, PhD Thesis,

Далее запись (, ) (или (, )) используется для обозна­ чения множеств всех конечных (бесконечных) блоков из состояния отно­ сительно множества наблюдаемых переходов. Если в качестве множества наблюдаемых переходов используется множество (, 0 ) для фик­ сированного множества переменных 0, то используется сокращённая запись } содержит все конечные блоки LTS (и только эти блоки).

3.6. Выводы В данной главе приведены основные понятия теории моделей программ, относящиеся к задаче верификации систем взаимодействующих процессов.

Приведены определения размеченных систем переходов и их параллельной композиции. Приведены определения сетевых грамматик, с помощью кото­ рых описывается топология распределённой системы. Указан способ порож­ дения модели (размеченной системы переходов) по параметризованному опи­ санию модели.

В приложении А приведены некоторые существующие отношения экви­ валентности и частичного порядка на размеченных системах переходов. Для успешного применения метода инвариантов (раздел 2.4) требуется выбрать отношение, удовлетворяющее свойствам монотонности для заданной опера­ ции параллельной композиции и консервативности для заданной темпораль­ ной логики. При этом, чем слабее выбранное отношение, тем большее мно­ жество LTS находится в заданном отношении и тем проще осуществляется поиск инварианта параметризованного семейства. В данной работе использу­ ются ослабленные отношения на моделях для поиска сетевых инвариантов среди LTS, выводимых из нетерминалов сетевой грамматики, без дополни­ тельной модификации LTS процессов.

Для отношений эквивалентности на моделях известны как отношения строгой бисимуляции, так и ослабленные варианты этого отношения. Одним из ослабленных отношений эквивалентности является отношение блочной би­ симуляции [20], в тоже время это отношение строже отношений ветвящейся и прореженной бисимуляции. В отличие от ветвящейся бисимуляции, отно­ шение блочной бисимуляции учитывает дивергенцию, т.е. бесконечные по­ следовательности ненаблюдаемых переходов. По этим причинам отношение блочной бисимуляции является одним из кандидатов на применение в методе сетевых инвариантов.

В данной работе вводится отношение блочной симуляции, отличающееся от отношения блочной бисимуляции отсутствием свойства симметричности.

Подобное отношение использовалось для теоретического обоснования мето­ дов редукции частичных порядков в работе [78].

Как и в случае блочной бисимуляции, отношение блочной симуляции строже отношений ветвящейся и прореженной симуляции. Отношение блоч­ ной симуляции обладает свойством консервативности, но не обладает свой­ ством монотонности. По этой причине мы ввели ослабленное отношение ква­ зиблочной симуляции, обладающее свойствами консервативности и монотон­ ности. Отношение квазиблочной симуляции используется, в основном, для теоретического обоснования метода, в то время как отношение блочной симу­ ляции используется для поиска инвариантов на практике.

В данном разделе определяются введённые нами отношения блочной и квазиблочной симуляции, доказываются основные свойства приведённых от­ ношений. Далее вводится отношение полублочной симуляции, с помощью ко­ торого можно уменьшить число сравниваемых состояний, показывается, что существование отношения полублочной симуляции является необходимым и достаточным условием существования отношения блочной симуляции. Для систем, свободных от внутренних тупиков, вводится упрощённый критерий существования отношения полублочной симуляции.

4.1. Блочная симуляция, 0,,,,, = 1, 2, с выделенным множеством наблюдаемых пе­ ременных 0 1 2. Отношение 1 2 называется блочной симуля­ цией на моделях 1 и 2 относительно 0, тогда и только тогда, когда для любой пары состояний (1, 1 ) выполняются следующие условия:

С помощью записи 1 bks 2 обозначим существование такого отно­ шения 1 2, что является блочной симуляцией на 1 и 2 от­ носительно 0, и для каждого начального состояния 0 1 найдётся такое начальное состояние 0 2, что (0, 0 ).©Igor

V. Konnov, PhD Thesis,

Отношение блочной симуляции является более слабым, чем отношение строгой симуляции. По этой причине класс пар моделей, находящихся в от­ ношении блочной симуляции, более многочислен, чем класс тех пар моделей, которые находятся в отношении строгой симуляции. Отношение блочной си­ муляции близко к отношению блочной бисимуляции [20], однако в нём не используется свойство симметричности. Определение отношения блочной си­ муляции схоже с определением наблюдаемой симуляции (visible simulation), используемой в работах [3] и [77].

Пример 4.1. Пусть 1 и 2 — размеченные системы переходов. Отношения переходов LTS изображены на рисунке 4.1. Системы переходов 1 и 2 на­ ходятся в отношении блочной симуляции, т.е. 1 bks 2.

Определение 4.2. Пусть даны LTS =, 0,,,,, = 1, 2, и отношение блочной симуляции 1 2 относительно множества наблюда­ моделей 1 и 2 называются -соответствующими, если для всякого Рисунок 4.1. Пример LTS, находящихся в отношении блочной симуляции -соответствующие пути и будем обозначать следующим образом:

Утверждение 4.1. Если даны такие пути = 1 2, = 1 2, что

1 1 и 2 2, то.©Igor V. Konnov, PhD Thesis,

относительно множества наблюдаемых переменных 0 1 2. Тогда для любой пары состояний 1 1, 1 2, находящихся в отношении блоч­ ной симуляции (1, 1 ), и любого пути из состояния 1 найдётся -соответствующий путь из состояния 1.

Доказательство. Пусть представляется единственным образом в виде ко­ нечной или бесконечной последовательности блоков = 1 · · ·...

(последний блок может быть бесконечным). -соответствующий путь стро­ ится индукцией по количеству блоков в префиксе 1 · · · пути.

Пусть = 1. Блок 1 выходит из состояния и (1, 1 ). Тогда по определению блочной симуляции найдётся такой блок 1 из состояния Пусть > 1. По предположению индукции построены такие блоки блоки могут находиться только в конце пути). Так как, то (+1, +1 ). По определению блочной симуляции для блока + найдётся такой блок +1, что +1 +1.

Для каждого префикса пути 1 · · · пути мы можем построить такой префикс 1 · · · пути, что 1 · · · 1 · · ·. Следовательно, для пути = 1 · · ·... можно построить такой путь = 1 · · ·..., что. Что и требовалось доказать.

Отношение блочной симуляции обладает свойством консервативности от­ шение блочной симуляции 1 2 относительно множества наблюда­ емых переменных 0 1 2.

Для любой пары состояний (1, 1 ) и любой формулы логики с переменными из множества 0 верно:

ACTL -X Доказательство. Докажем перекрёстной индукцией по длине формулы расширенное утверждение:

Для любой пары состояний (1, 1 ) и любой такой формулы состо­.©Igor V. Konnov, PhD Thesis, Для любой пары -соответствующих путей = 1 · · ·..., = Доказательство расширенного утверждения.

1. Пусть — формула состояния, || = 1 (формул пути длины 1 быть не 2. Пусть для любой формулы состояния, || <, и любой формулы пути , || <, верно расширенное утверждение. Докажем утверждение для формул длины.

а. Пусть = ¬, 0, — формула состояния. Поскольку 2, |= в. Пусть = 1 2 ( = 1 2 ) — формула пути. Так как 2, |=, то 2, |= 1 или (и) 2, |= 2. По предположению индукции г. Пусть = G — формула пути, — формула состояния.

Так как 2, |= G, то для всех 1 и всех состояний блока Из 2, |= для всех таких, что 1, и соотношения (4.1) по предположению индукции следует: 1, |= для всех таких, Следовательно, для любого состояния пути верно 1, |=.

Поэтому выполняется 1, |= G.

д. Пусть = 1 U2 — формула пути, 1, 2 — формулы состояния.

Поскольку 2, |= 1 U2, найдутся такие числа 1, 1, что выполняются соотношения:

1 ;©Igor V. Konnov, PhD Thesis, для всех состояний любого блока, где <, верно 2, |= верно (, ) и 2, |= 1. Следовательно, по предположению Покажем, что из выполнимости формулы на любом пути модели 2 следует выполнимость формулы на любом пути модели 1.

Возьмём произвольный путь модели 1 из состояния. Так как (, ), по лемме 4.2 найдётся такой -соответствующий путь верно 2, |=. По предположению индукции из выполнимости Из пунктов 1 и 2а– 2е следуют расширенное утверждение и утверждение теоремы.©Igor V. Konnov, PhD Thesis, Если в определении 4.1 потребовать выполнение свойства симметрично­ сти отношения, отношение будет отношением блочной бисимуляции, определённым в работе [20].

4.2. Квазиблочная симуляция Определение 4.3 (Квазиблочная симуляция, qbs). Пусть заданы LTS =, 0,,,,, = 1, 2, с выделенным множеством наблюдаемых пере­ менных 0 1 2. Пусть также заданы множества наблюдаемых переходов 1 и 2 моделей 1 и 2 соответственно. Отношение 1 2 называется квазиблочной симуляцией на моделях 1 и 2 относительно множеств 0, 1, 2, если для любой пары состояний (1, 1 ) выполняются следующие условия:

(1, 1 ) модели 1 найдётся такой соответствующий блок = (1, 1 ) модели 1 найдётся такой соответствующий бесконеч­ Для LTS 1 и 2 мы будем использовать запись 1 0 2, если най­ дутся два множества наблюдаемых переходов 1, 2 моделей 1, 2 соответ­ ственно и такое отношение квазиблочной симуляции 1 2 относитель­ но 0, 1, 2, в котором для каждого начального состояния 0 1 найдётся такое соответствующее начальное состояние 0 2, что (0, 0 ).©Igor Konnov, PhD Thesis, Если множества наблюдаемых переходов 1 и 2 согласованы относи­ тельно заданной формулы, то отношение квазиблочной симуляции так же называется согласованным относительно формулы.

4.2.1. Свойства квазиблочной симуляции Из определений блочной и квазиблочной симуляции следует, что отно­ шение блочной симуляции является и отношением квазиблочной симуляции.

Утверждение 4.4. Пусть заданы LTS =, 0,,,,, = 1, 2, с множеством наблюдаемых переменных 0 1 2. Если — отношение блочной симуляции для множества переменных 0, то — отношение квазиблочной симуляции для множеств наблюдаемых переходов 1 = (1, 0 ) и 2 = (2, 0 ) и множества наблюдаемых переменных 0.

Построение отношения квазиблочной симуляции при заданных множе­ ствах наблюдаемых переходов 1 и 2 можно свести к построению блочной симуляции. Пусть заданы LTS =, 0,,,,, = 1, 2, с множе­ ством наблюдаемых переменных 0 1 2 и множествами наблюдаемых переходов 1, 2. Добавим дополнительное наблюдаемое действие удовлетворяющие следующим условиям:©Igor V. Konnov, PhD Thesis, множеством наблюдаемых переменных 0 1 2 верно:

Одним из основных свойств квазиблочной симуляции является свойство монотонности.

Теорема 4.6. Пусть заданы:

такие непересекающиеся множества переменных и, что Тогда из 1 qbs 2 и 3 qbs 4 следует 1 3 qbs 2 4.

Для доказательства теоремы введём определение проекции модели.