2014-10-10 128 views
2

是否有正式/传统的方式来描述数据/命令交换协议?例如,对于编程语言,有多种方法来描述语法和语义(如:http://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form)。正式描述协议的方式

我正在寻找的方法是相当实用的(与学术相反)。我需要一些日常用于数据交换描述的同时处理规范,只是为了向其他人传达/清晰地传达想法。所以,如果有些东西不被认为是事实上的标准,但是有用的 - 它也可以。

我看了一下UML序列图和“通信协议规范和验证的正式方法”,由卡尔A.阳光,1979年。前一种方法没有描述“有效载荷”(至少从我所理解的内容中),而后一种方法是一种描述考虑因素而非方法的教育性论文(尽管我仍在阅读本文)。

在此先感谢

回答

1

协议是关于根据一系列交互发送的消息。

指定我见过的协议的最佳方式是使用Colored Petri Nets (CPNs)

CPN基于(“无色”)Petri Nets (PNs),它定义了并行活动如何通过使用位置来表示可能的状态,令牌就地表示状态以及转换(同步)来同步比如消息响应,指明平行国家必须在哪些方面取得进展。 Petri网可以模拟有限状态机(FSA是一个总是具有“单一令牌”的PN,例如“当前状态”),所以是泛化;事实上,它们可以将某些FSA“指数地压缩”为非常小的描述,因此即使对于复杂的交互序列也可以非常简洁。但是传统的PN不能解决正在交换的数据。

CPN概括PN以添加数据类型。令牌现在具有“颜色”(有趣的方式称为“数据类型”),并且转换不仅可以同步,还可以将令牌组合成令牌以生成其他令牌,例如计算新值。

建模为CPN的协议因此具有作为数据类型的消息内容,并且PN指示同步。如果您从未使用过CPN,那么了解它们的真实含义是非常值得的,因为它们非常适合FSA。

关于OP的“功利主义”评论,CPN Tools有非常好的工具,包括图形建模和代码生成。

0

对于它的价值,因为你提到BNF:我相信我已阅读,维尔特使用EBNF指定协议,用散文解释该字符串的部分是由客户端发出和哪些部分由服务器完成。我无法找到手边的参考资料,但我记得我读过的例子比我在别处读过的大多数协议描述更清楚。

+2

BNF是模拟协议一个糟糕的方式。它并没有模拟值得一提的状态。 (你可能能够定义字符串来回,但大多数BNF是上下文无关的,这意味着“没有太多的过去的记忆(左上下文)”,它可能用于模型消息结构。但是你可能想要一个更复杂的模型涉及到约束;检查XML Schemas是一个更复杂的数据建模工具,它是BNF的一个超集。 – 2014-12-08 18:17:49

+1

我怀疑Wirth将协议的定义限制为EBNF可以捕获的协议的定义,不仅限于他禁止声明之前使用他的编程语言中的规则和类型声明,但是...点好了(我一定会看看XSD ... :-) – 2014-12-09 01:16:09

1

在电信方面,描述网元间相互作用的标准是Z.100 : Specification and Description Language (SDL)和配套Z.120 : Message Sequence Chart (MSC)建议。该套件包含一个测试框架。

数学上更弯曲的方法是使用某种类型的各种状态机模型。

早期出版物之一Design and Validation of Computer Protocols(1991)由Gerard Holzmann撰写,描述了SPIN模型检查器和PROMELA语言。

TLA +,Petri-nets,Alloy,CSP,Z等几乎任何其他符号也可用于推理协议,而且选择通常取决于熟悉度和工具可用性。

如果严谨并不重要,那么Harel state charts提供了许多工程师熟悉的符号。

基本上,序列图本身的问题在于它们描述了通过协议的单个跟踪。他们不容易表现出描述并行操作所需的非确定性,并且难以简洁地表示选择。当用分层消息图表(HMC)扩展时,它们会回落到状态机空间中。

1

如果你认为“功利”是指“有用”,那么考虑Petri网。请参阅下面的回复或考虑回复的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

+0

你应该同意在这种形式下很难描述每一个值被传送和每一位被检查。 但是为了提出协议它可能是有用的,我同意。谢谢你的回答。 – 2015-04-08 20:30:29

+0

我还没有三编辑来描述位级的协议。我确实同意,看起来好像用Petri网来描述这个级别是有挑战性的。看到在这些描述中会遇到的挑战类型以及是否有系统的方法来缓解描述,以明确映射到Petri Net元素,这将是有趣的。 – 2015-04-08 22:43:38

+0

对不起,我不理解你的评论(你在问哪种挑战是系统性的)。请用实例详细说明。我看到的挑战是,用这种表示方式描述会过于庞大。我假设,带有左侧和右侧列(代表接收器和发射器)的纯文本格式不太正式,但更适用。 – 2015-04-09 10:48:49