Анализ доступности - Reachability analysis

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

Обзор

Анализ достижимости был представлен в статье 1978 года для анализа и проверки протоколы связи.^[1]. Эта статья была вдохновлена статьей Бартлетта и др. 1968 года ^[2] который представил чередующийся битовый протокол используя моделирование сущностей протокола с конечным числом состояний, а также указал, что аналогичный протокол, описанный ранее, имел конструктивный недостаток. Этот протокол принадлежит Связующий слой и, при определенных предположениях, предоставляет в качестве услуги правильную доставку данных без потерь или дублирования, несмотря на случайное присутствие повреждения или потери сообщения.

Для анализа достижимости локальные сущности моделируются по их состояниям и переходам. Сущность изменяет состояние, когда она отправляет сообщение, потребляет полученное сообщение или выполняет взаимодействие на своем локальном сервисном интерфейсе. Глобальное состояние ${ displaystyle s = (s_ {1}, s_ {2}, ..., s_ {n}, средний)}$ системы с n объектами ^[3] определяется состояниями ${ displaystyle s_ {i}}$ (i = 1, ... n) сущностей и состояние связи ${ displaystyle medium}$ . В простейшем случае среда между двумя объектами моделируется двумя очередями FIFO в противоположных направлениях, которые содержат сообщения в пути (которые отправлены, но еще не потреблены). Анализ достижимости рассматривает возможное поведение распределенной системы путем анализа всех возможных последовательностей переходов состояний объектов и соответствующих достигнутых глобальных состояний. ^[4].

Результатом анализа достижимости является глобальный граф переходов между состояниями (также называемый графом достижимости), который показывает все глобальные состояния распределенной системы, которые достижимы из начального глобального состояния, и все возможные последовательности взаимодействий отправки, потребления и обслуживания, выполняемые локальным сущности. Однако во многих случаях этот граф переходов не ограничен и не может быть исследован полностью. Граф переходов может использоваться для проверки общих недостатков конструкции протокола (см. Ниже), а также для проверки того, что последовательности сервисных взаимодействий между объектами соответствуют требованиям, заданным глобальной сервисной спецификацией системы. ^[1].

Свойства протокола

Ограниченность: Граф глобальных переходов состояний ограничен, если количество сообщений, которые могут быть в передаче, ограничено, а число состояний всех объектов ограничено. Вопрос о том, остается ли количество сообщений ограниченным в случае конечных объектов, в общем случае не разрешимый ^[5]. Обычно исследование графа переходов обрезается, когда количество сообщений в пути достигает заданного порога.

Ниже приведены недостатки конструкции:

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

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

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

Пример

На схеме показаны два объекта протокола и сообщения, которыми обмениваются они.

На схеме показаны два конечных автомата, которые определяют динамическое поведение соответствующих протокольных объектов.

На этой диаграмме показана модель конечного автомата глобальной системы, состоящая из двух протокольных объектов и двух каналов FIFO, используемых для обмена сообщениями между ними.

В качестве примера рассмотрим систему из двух протокольных сущностей, которые обмениваются сообщениями ма, мб, MC и мкр друг с другом, как показано на первой диаграмме. Протокол определяется поведением двух объектов, которое показано на второй диаграмме в виде двух конечных автоматов. Здесь символ "!" означает отправку сообщения, а "?" означает использование полученного сообщения. Начальные состояния - это состояния «1».

На третьей диаграмме показан результат анализа достижимости для этого протокола в виде глобального конечного автомата. Каждое глобальное состояние имеет четыре компонента: состояние объекта протокола A (слева), состояние объекта B (справа) и сообщения в пути в середине (верхняя часть: от A до B; нижняя часть: от B до A. ). Каждый переход этого глобального конечного автомата соответствует одному переходу объекта протокола A или объекта B. Начальное состояние - [1, - -, 1] (нет сообщений в пути).

Видно, что этот пример имеет ограниченное глобальное пространство состояний - максимальное количество сообщений, которые могут передаваться одновременно, равно двум. Этот протокол имеет глобальный тупик, который находится в состоянии [2, - -, 3]. Если убрать переход A в состояние 2 для потребления сообщения мб, в глобальных состояниях будет неуказанный прием [2, ма мб , 3] и [2, - мб ,3].

Передача сообщений

Дизайн протокола должен быть адаптирован к свойствам базовой среды связи, к возможности отказа партнера по связи и к механизму, используемому объектом для выбора следующего сообщения для использования. Среда связи для протоколов на Уровень связи обычно ненадежен и допускает ошибочный прием и потерю сообщения (моделируется как изменение состояния среды). Протоколы, использующие IP-службу Интернета, также должны учитывать возможность доставки с нарушением порядка. Протоколы более высокого уровня обычно используют ориентированную на сеанс транспортную службу, что означает, что среда обеспечивает надежную передачу сообщений FIFO между любой парой объектов. Однако при анализе распределенные алгоритмы, часто принимают во внимание возможность того, что какой-то объект полностью выйдет из строя, что обычно обнаруживается (например, потеря сообщения в среде) с помощью тайм-аут механизм, когда ожидаемое сообщение не приходит.

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

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

Несколько очередей: Каждый объект имеет несколько очередей FIFO, по одной для каждого взаимодействующего партнера. Здесь объект имеет возможность решить, в зависимости от своего состояния, из какой очереди (или очередей) должно быть получено следующее входное сообщение.

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

Оригинальная статья, определяющая проблему неуточненных приемов ^[6], и большая часть последующей работы предполагала одну входную очередь ^[7]. Иногда неуказанные приемы вводятся состояние гонки, что означает, что получены два сообщения, и их порядок не определен (что часто бывает, если они приходят от разных партнеров). Многие из этих недостатков дизайна исчезают при использовании нескольких очередей или пулов приема. ^[8]. При систематическом использовании пулов приема анализ достижимости должен проверять частичные взаимоблокировки и сообщения, навсегда остающиеся в пуле (не потребляемые объектом) ^[9]

Практические вопросы

Большая часть работы по моделированию протокола используется конечные автоматы (FSM) для моделирования поведения распределенных объектов (см. Также Связь с конечными автоматами ). Однако этой модели недостаточно для моделирования параметров сообщений и локальных переменных. Поэтому часто используются так называемые расширенные модели конечных автоматов, поддерживаемые такими языками, как SDL или Конечные автоматы UML. К сожалению, для таких моделей анализ достижимости становится намного сложнее.

Практическим вопросом анализа достижимости является так называемый «взрыв в пространстве состояний». Если два объекта протокола имеют 100 состояний каждый, а среда может включать 10 типов сообщений, до двух в каждом направлении, то количество глобальных состояний в графе достижимости ограничивается числом 100 x 100 x (10 x 10) x (10 x 10), что составляет 100 миллионов. Поэтому был разработан ряд инструментов для автоматического выполнения анализа достижимости и проверки модели на графе достижимости. Мы упоминаем только два примера: Проверка модели SPIN и набор инструментов для построение и анализ распределенных процессов.

дальнейшее чтение

Протоколы связи
Джеральд Хольцманн: Разработка и проверка компьютерных протоколов, Prentice Hall, 1991.
G.v. Бохманн, Д. Райнер и Ч. Запад: Некоторые заметки по истории разработки протоколов, журнал Computer Networks, 54 (2010), стр 3197–3209.

Ссылки и примечания

^ ^а ^б Бохманн, Г.В. "Описание протоколов связи в компьютерных сетях с помощью конечного состояния, том 2 (1978), стр. 361-372". Цитировать журнал требует | журнал = (Помогите)
^ К.А. Бартлетт, Р.А. Скантлбери и П. Уилкинсон, Заметка о надежной полнодуплексной передаче по полудуплексным каналам, C.ACM 12, 260 (1969).
^ Примечание: в случае анализа протокола обычно есть только два объекта.
^ Примечание. Повреждение или потеря сообщения моделируется как изменение состояния ${ displaystyle medium}$ .
^ М.Г. Гауда, Э.Г. Маннинг, Ю.Т.Ю: О развитии связи между двумя конечными автоматами, Дои
^ П. Зафиропуло, К. Уэст, Х. Рудин, Д. Коуэн, Д. Бранд: На пути к анализу и синтезу протоколов, IEEE Transactions on Communications (том: 28, выпуск: 4, апрель 1980 г.)
^ Примечание: конструкция SAVE SDL может использоваться, чтобы указать, что определенные типы сообщений не должны использоваться в текущем состоянии, а должны сохраняться для будущей обработки.
^ М.Ф. Аль-Хаммури и Г.В. Бохманн: Возможность реализации сервисных спецификаций, Proc. Конференция по системному анализу и моделированию (SAM) 2018, Копенгаген, LNCS, Springer
^ К. Фурне, Т. Хоар, С. К. Раджамани и Дж. Реоф: Соответствие свободным от застреваний, Proc. 16-й международный Конф. по компьютерной проверке (CAV’04), LNCS, vol. 3114, Springer, 2004 г.

[Boch78-1] а ^б Бохманн, Г.В. "Описание протоколов связи в компьютерных сетях с помощью конечного состояния, том 2 (1978), стр. 361-372". Цитировать журнал требует | журнал = (Помогите)

[2] К.А. Бартлетт, Р.А. Скантлбери и П. Уилкинсон, Заметка о надежной полнодуплексной передаче по полудуплексным каналам, C.ACM 12, 260 (1969).

[3] Примечание: в случае анализа протокола обычно есть только два объекта.

[4] Примечание. Повреждение или потеря сообщения моделируется как изменение состояния ${ displaystyle medium}$ .

[5] М.Г. Гауда, Э.Г. Маннинг, Ю.Т.Ю: О развитии связи между двумя конечными автоматами, Дои

[6] П. Зафиропуло, К. Уэст, Х. Рудин, Д. Коуэн, Д. Бранд: На пути к анализу и синтезу протоколов, IEEE Transactions on Communications (том: 28, выпуск: 4, апрель 1980 г.)

[7] Примечание: конструкция SAVE SDL может использоваться, чтобы указать, что определенные типы сообщений не должны использоваться в текущем состоянии, а должны сохраняться для будущей обработки.

[8] М.Ф. Аль-Хаммури и Г.В. Бохманн: Возможность реализации сервисных спецификаций, Proc. Конференция по системному анализу и моделированию (SAM) 2018, Копенгаген, LNCS, Springer

[9] К. Фурне, Т. Хоар, С. К. Раджамани и Дж. Реоф: Соответствие свободным от застреваний, Proc. 16-й международный Конф. по компьютерной проверке (CAV’04), LNCS, vol. 3114, Springer, 2004 г.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]