Войти
Анализ достижимости решение проблемы достижимости в конкретном контексте распределенных систем. Он используется для определения того, какие глобальные состояния могут быть достигнуты распределенной системой, состоящей из определенного числа локальных объектов, которые обмениваются сообщениями.
Анализ доступности был представлен в статье 1978 года для анализа и проверки протоколов связи. Эта статья была вдохновлена статьей Бартлетта и др. от 1968 г., в котором был представлен протокол с чередованием битов с использованием моделирования объектов протокола с конечным числом состояний, а также отмечалось, что аналогичный протокол, описанный ранее, имел конструктивный недостаток. Этот протокол принадлежит к канальному уровню и, при определенных предположениях, обеспечивает в качестве услуги правильную доставку данных без потерь или дублирования, несмотря на случайное присутствие повреждения или потери сообщения.
Для анализа достижимости локальные объекты моделируются их состояниями и переходами. Сущность изменяет состояние, когда она отправляет сообщение, потребляет полученное сообщение или выполняет взаимодействие на своем локальном сервисном интерфейсе. Глобальное состояние 
Результатом анализа достижимости является глобальный граф переходов состояний (также называемый графом достижимости), который показывает все глобальные состояния распределенной системы, достижимые из начального глобального состояния, а также все возможные последовательности отправки, потребления и сервисные взаимодействия, выполняемые местными организациями. Однако во многих случаях этот граф переходов не ограничен и не может быть исследован полностью. Граф переходов можно использовать для проверки общих недостатков конструкции протокола (см. Ниже), а также для проверки того, что последовательности сервисных взаимодействий между объектами соответствуют требованиям, заданным глобальной сервисной спецификацией системы.
Ограниченность: глобальный граф переходов между состояниями ограничен, если количество сообщений, которые могут быть в пути, ограничено, а количество состояний всех объектов ограничено. Вопрос о том, остается ли количество сообщений ограниченным в случае объектов с конечным состоянием, обычно не разрешим. Обычно исследование графа переходов обрезается, когда количество сообщений в пути достигает заданного порога.
Ниже перечислены недостатки конструкции:
На схеме показаны два объекта протокола и сообщения, которыми обмениваются между ними. 
На схеме показаны два конечных автомата, которые определяют динамическое поведение соответствующих протокольных объектов. 
На этой диаграмме показана модель конечного автомата глобальной системы, состоящая из двух протокольных объектов и двух каналов FIFO, используемых для обмена сообщениями между ними. В качестве примера мы рассмотрим систему из двух протокольных объектов, которые обмениваются сообщениями ma, mb, mc и md друг с другом, как показано на первой диаграмме. Протокол определяется поведением двух объектов, которое показано на второй диаграмме в виде двух конечных автоматов. Здесь символ "!" означает отправку сообщения, а "?" означает использование полученного сообщения. Начальные состояния - это состояния «1».
На третьей диаграмме показан результат анализа достижимости для этого протокола в виде глобального конечного автомата. Каждое глобальное состояние имеет четыре компонента: состояние объекта протокола A (слева), состояние объекта B (справа) и сообщения в пути в середине (верхняя часть: от A до B; нижняя часть: от B до A.). Каждый переход этого глобального конечного автомата соответствует одному переходу объекта протокола A или объекта B. Начальное состояние - [1, - -, 1] (нет сообщений в пути).
Видно, что этот пример имеет ограниченное глобальное пространство состояний - максимальное количество сообщений, которые могут передаваться одновременно, равно двум. Этот протокол имеет глобальный тупик, который находится в состоянии [2, - -, 3]. Если удалить переход A в состояние 2 для потребления сообщения mb, будет неуказанный прием в глобальных состояниях [2, ma mb, 3] и [2, - mb, 3].
Дизайн протокола должен быть адаптирован к свойствам базовой среды связи, к возможности сбоя партнера по обмену данными и к механизму, используемому объектом для выберите следующее сообщение для потребления. Среда связи для протоколов на канальном уровне обычно ненадежна и допускает ошибочный прием и потерю сообщений (моделируется как переход состояния среды). Протоколы, использующие IP-службу Интернета, также должны учитывать возможность доставки с нарушением порядка. Протоколы более высокого уровня обычно используют ориентированную на сеанс транспортную службу, что означает, что среда обеспечивает надежную передачу сообщений FIFO между любой парой объектов. Однако при анализе распределенных алгоритмов часто учитывается возможность полного отказа какого-либо объекта, что обычно обнаруживается (например, потеря сообщения в носителе) с помощью таймаута механизм, когда ожидаемое сообщение не приходит.
Были сделаны различные предположения о том, может ли объект выбрать конкретное сообщение для использования, когда несколько сообщений прибыли и готовы к употреблению. Основными моделями являются следующие:
Исходный документ, определяющий проблему неуказанных приемов, и большая часть последующей работы предполагали единственную входную очередь. Иногда неуказанные приемы вводятся из-за состояния гонки, что означает, что получены два сообщения и их порядок не определен (что часто бывает, если они приходят от разных партнеров). Многие из этих конструктивных недостатков исчезают при использовании нескольких очередей или пулов приема. При систематическом использовании пулов приема анализ достижимости должен проверять частичные взаимоблокировки и сообщения, навсегда остающиеся в пуле (не потребляемые объектом)
Большая часть работы по протоколу при моделировании используются конечные автоматы (FSM) для моделирования поведения распределенных объектов (см. также Обмен данными между конечными автоматами ). Однако этой модели недостаточно для моделирования параметров сообщений и локальных переменных. Поэтому часто используются так называемые расширенные модели конечных автоматов, поддерживаемые такими языками, как SDL или конечные автоматы UML. К сожалению, для таких моделей анализ достижимости становится намного сложнее.
Практическая проблема анализа достижимости - это так называемый «взрыв пространства состояний». Если два объекта протокола имеют 100 состояний каждый, а среда может включать 10 типов сообщений, до двух в каждом направлении, то количество глобальных состояний в графе достижимости ограничивается числом 100 x 100 x (10 x 10) x (10 x 10), что составляет 100 миллионов. Поэтому был разработан ряд инструментов для автоматического выполнения анализа достижимости и проверки модели на графе достижимости. Мы упоминаем только два примера: средство проверки модели SPIN и набор инструментов для построения и анализа распределенных процессов.
