Formal way to describe protocols
Is there a formal/traditional way to describe data/command exchange protocols? For example, for programming languages there are multiple approaches to describe the syntax and semantics (like: http://en.wikipedia.org/wiki/Backus%E2%80%93Naur_Form).
The approach I am looking for is rather utilitarian (in contrast to academic). I need something for day-to-day use for data exchange description while working on specifications, just to transfer/spread clearly the idea to others. So, if there is something that is not recognized as a de-facto standard but is useful - it is ok too.
I took a look at UML sequence diagrams and "Formal Methods for Communication Protocol Specification And Verification, by Carl A. Sunshine, 1979". Former method is missing the description of "payloads" (at least from what I understood) while latter one is rather an educative paper describing considerations rather than methods (I am still going through this paper, though).
Thanks in advance
Protocols are about messages sent in accordance to a series of interactions.
The best way to specify protocols that I have seen is with Colored Petri Nets (CPNs).
CPNs are based on ("uncolored") Petri Nets (PNs), which define how parallel activities synchronize, eg, the message responses, by using Places to represent possible states, Tokens-in-places to represent state, and transition (synchronization) gates to indicate where parallel states must coincide to make progress. Petri Nets can model Finite State Machines (an FSA is a PN that always has a "single token", eg, the "current state") and so are a generalization; in fact, they can "exponentially compress" certain FSAs into very small descriptions and can thus be quite succinct even for complex interaction sequences. But a conventional PN does not address the data being exchanged.
CPNs generalize PNs to add data types. The tokens now have "colors" (funny way to say "data type") and transitions can not only synchronize but can combine tokens to produce other tokens, eg, compute new values.
A protocol modelled as CPN thus has message content as data types, and PNs states to indicate the syncronization. If you've never used a CPN, it is really worth your trouble to learn what they are, because they are such a pretty generalization of FSAs.
Regarding OPs' "utilitarian" remark, there are very good tools available at CPN Tools, including graphical modelling and code generation.
In telecommunications, the standard for describing interaction between network elements is Z.100 : Specification and Description Language (SDL) and the companion Z.120 : Message Sequence Chart (MSC) recommendations. The suite includes a testing framework.
A more mathematically bent approach would be to use various state machine models of some type.
One of the early publications, Design and Validation of Computer Protocols (1991), was written by Gerard Holzmann to describe the SPIN model checker and the PROMELA language.
Almost any other notation like TLA+, Petri-nets, Alloy, CSP, Z, ... can also be used to reason about protocols and the choice often depends on familiarity and tools availability.
If rigour is not essential, then Harel state charts provide a notation familiar to many engineers.
Fundamentally, the problem with sequence charts on their own is that they describe a single trace through the protocol. They cannot easily show the non-determinism required to describe parallel operations, and struggle to succinctly represent choice. When extended with hierarchical message charts (HMC) then they fall back into the state machine space.
If by "utilitarian" you mean "useful", consider Petri Nets. Please see my reply below or consider a PDF version of the reply.
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
链接地址: http://www.djcxy.com/p/21438.html上一篇: MySQL缺席报告脚本
下一篇: 描述协议的正式方式