Формальный способ описания протоколов

Question

Существует ли формальный/традиционный способ описания протоколов обмена данными/командами? Например, для языков программирования существует несколько подходов к описанию синтаксиса и семантики (например: http://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form).

Подход, который я ищу, довольно утилитарный (в отличие от академического). Мне нужно что-то для повседневного использования для описания обмена данными при работе над спецификациями, просто для передачи/распространения идеи другим. Итак, если есть что-то, что не признано де-факто стандартом, но полезно - все в порядке.

Я взглянул на диаграммы последовательности UML и «Формальные методы для спецификации и проверки протокола связи, Carl A. Sunshine, 1979». В прежнем методе отсутствует описание «полезных нагрузок» (по крайней мере, из того, что я понял), в то время как последний является скорее учебным документом, описывающим соображения, а не методы (хотя я все еще просматриваю эту статью).

Заранее спасибо

Answer 1

Протоколы - это сообщения, отправленные в соответствии с рядом взаимодействий.

Лучший способ указать протоколы, которые я видел, - Colored Petri Nets (CPNs).

CPN основаны на («неокрашенном») Petri Nets (PNs), которые определяют, как синхронизировать параллельные действия, например, ответы сообщений, используя точки для представления возможных состояний, токены в местах для представления состояния и перехода (синхронизации) чтобы указать, где параллельные состояния должны совпадать, чтобы добиться прогресса. Сети Петри могут моделировать конечные государственные машины (FSA - это PN, который всегда имеет «единственный токен», например «текущее состояние»), и, следовательно, является обобщением; на самом деле, они могут «экспоненциально сжимать» определенные FSA в очень мелкие описания и, таким образом, могут быть весьма краткими даже для сложных последовательностей взаимодействия. Но обычное ПШ не относится к обмену данными.

CPNs обобщают PN для добавления типов данных. Теперь у токенов есть «цвета» (забавный способ сказать «тип данных»), и переходы могут не только синхронизироваться, но и объединять маркеры для создания других токенов, например, вычислять новые значения.

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

Что касается «утилитарного» замечания OPs, то есть очень хорошие инструменты, доступные по адресу CPN Tools, включая графическое моделирование и генерацию кода.

Answer 2

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

Answer 3

В телекоммуникациях стандартом для описания взаимодействия между сетевыми элементами является Z.100 : Specification and Description Language (SDL) и рекомендация компаньона Z.120 : Message Sequence Chart (MSC). В комплект поставки входит платформа тестирования.

Более математически изогнутый подход заключается в использовании различных моделей государственных машин определенного типа.

Одна из ранних публикаций, Design and Validation of Computer Protocols (1991), была написана Джерардом Хольцманом для описания проверки модели SPIN и языка ПРОМЕЛА.

Практически любые другие обозначения, такие как TLA +, Petri-nets, Alloy, CSP, Z, ... также могут использоваться для разбора протоколов, и выбор часто зависит от доступности и доступности инструментов.

Если строгость не является обязательной, то Harel state charts представляют собой обозначения, знакомые многим инженерам.

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

Answer 4

Если «утилитарный» означает «полезный», рассмотрите Петри Сети. См. Мой ответ ниже или рассмотрите ответ PDF version.

first page of reply http://www.aespen.ca/AEnswers/lMtbX1428143440-0_Page_1.jpg second page of reply http://www.aespen.ca/AEnswers/lMtbX1428143440-0_Page_2.jpg