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

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

Лучший способ указать протоколы, которые я видел, — использовать цветные сети Петри (CPN).

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

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

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

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

В области электросвязи стандартом описания взаимодействия между сетевыми элементами является Z.100: Спецификация и описание. Язык (SDL) и сопутствующий Z.120: Message Sequence Chart ( MSC) рекомендации. В комплект входит среда тестирования.

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

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

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

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

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

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

http://www.aespen.ca/AEnswers/lMtbX1428143440-0_Page_1.jpg http://www.aespen.ca/AEnswers/lMtbX1428143440-0_Page_2.jpg

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