91:
50:), the definition of the protocol of a specific layer should be such that any entity implementing that specification in one computer would be compatible with any other computer containing an entity implementing the same specification, and their interactions should be such that the desired communication service would be obtained. On the other hand, the protocol specification should be abstract enough to allow different choices for the implementation on different computers.
83:
128:. Protocol conformance testing checks that a given entity implementation conforms to the protocol specification. The conformance test cases are developed based on the protocol specification and are applicable to all entity implementations. Therefore standard conformance test suites have been developed for certain protocol standards.
150:. However, finite-state descriptions are not powerful enough to describe constraints between message parameters and the local variables in the entities. Such constraints can be described by the standardized formal specification languages mentioned above, for which powerful tools have been developed.
120:
The development of an entity implementation. Note that the abstract properties of the service interface are defined by the service specification (and also used by the protocol specification), but the detailed nature of the interface can be chosen during the implementation process, separately for each
178:
Most protocols are designed by human intuition and discussions during the standardization process. However, some methods have been proposed for using constructive methods possibly supported by tools to automatically derive protocols that satisfy certain properties. The following are a few examples:
65:
It was also recognized that some kind of formalized protocol specification would be useful for the verification of the protocol and for developing implementations, as well as test cases for checking the conformance of an implementation against the specification. While initially mainly finite-state
53:
It was recognized that a precise specification of the expected service provided by the given layer was important. It is important for the verification of the protocol, which should demonstrate that the communication service is provided if both protocol entities implement the protocol specification
193:
Protocol for control applications: The specification of one entity (called the plant - which must be controlled) is given, and the method derives a specification of the other entity such that certain fail states of the plant are never reached and certain given properties of the plant's service
102:
Layered architecture: A protocol layer at the level n consists of two (or more) entities that have a service interface through which the service of the layer is provided to the users of the protocol, and which uses the service provided by a local entity of level
161:
as well as hardware design, especially for distributed and real-time systems. On the other hand, many methods and tools developed in the more general context of software engineering can also be used of the development of protocols, for instance
137:
Tools for the activities of protocol verification, entity implementation and test suite development can be developed when the protocol specification is written in a formalized language which can be understood by the tool. As mentioned,
186:
Synchronizing protocol: The state transitions of one protocol entity are given by the user, and the method derives the behavior of the other entity such that it remains in states that correspond to the former
183:
Semi-automatic protocol synthesis: The user defines all message sending actions of the entities, and the tool derives all necessary reception actions (even if several messages are in transit).
112:
Protocol verification consists of showing that two (or more) entities satisfying the protocol specification will provide at their service interfaces the specified service of that layer.
66:
machine were used as (simplified) models of a protocol entity, in the 1980s three formal specification languages were standardized, two by ISO and one by ITU. The latter, called
312:
P. Zafiropulo, C. West, H. Rudin, D. Cowan, D. Brand : Towards analyzing and synthesizing protocols, IEEE Transactions on
Communications ( Volume: 28, Issue: 4, Apr 1980 )
303:
G.J. Dickson ; P.E. de Chazal, Status of CCITT description techniques and application to protocol specification, Proceedings of the IEEE, vol. 71, 12, pp. 1346-1355 (1983).
321:
M.G. Gouda and Y.T. Yu, Synthesis of communicating Finite State
Machines with guaranteed progress, IEEE Trans. on Comm., vol. Com-32, No. 7, July 1984, pp. 779-788.
330:
M.F. Al-hammouri and G.v. Bochmann, Realizability of service specifications, Proc. System
Analysis and Modelling (SAM) conference 2018, Copenhagen, LNCS, Springer.
339:
G. v. Bochmann, Using logic to solve the submodule construction problem, Journal on
Discrete Event Dynamic Systems, Vol. 23 (1), Springer, March 2013, pp. 27-59.
106:
The service specification of a layer describes, in an abstract and global view, the behavior of the layer as visible at the service interfaces of the layer.
146:
was proposed to understand all possible behaviors of a distributed system, which is essential for protocol verification. This was later complemented with
190:
Protocol derived from service specification: The service specification is given by the user and the method derives a suitable protocol for all entities.
285:
G. v. Bochmann, D. Rayner and C. H. West, Some notes on the history of protocol engineering, Computer
Networks journal, 54 (2010), pp 3197–3209.
294:
C. A. Vissers, G. v. Bochmann and R. L. Tenney, Formal description techniques, Proceedings of the IEEE, vol. 71, 12, pp. 1356-1364, Dec. 1983.
260:
G. v. Bochmann and C. A. Sunshine, Formal methods in communication protocol design, IEEE Tr. COM-28, No. 4 (April 1980), pp. 624-631.
142:
languages have been proposed for protocol specification, and the first methods and tools where based on finite-state machine models.
67:
355:
109:
The protocol specification defines the requirements that should be satisfied by each entity implementation.
195:
167:
42:
were developed in the 1970s, the concept of protocols was not yet well developed. These were the first
154:
94:
Layered protocol architecture: More abstract view – showing the communication service provided.
23:
143:
43:
158:
139:
27:
8:
125:
115:
The (verified) protocol specification is used mainly for the following two activities:
90:
71:
39:
98:
The following are the most important principles for the development of protocols:
59:
163:
147:
54:
correctly. This principle was later followed during the standardization of the
349:
16:
Field that applies systematic methods for developing communication protocols
46:. In the context of the newly adopted layered protocol architecture (see
82:
270:
157:
was used very early. These methods and tools have later been used for
55:
47:
30:, but it is specific to the development of distributed systems.
22:
is the application of systematic methods to the development of
173:
70:, was later used in industry and has been merged with
347:
153:It is in the field of protocol engineering that
271:Protocol Specification Testing and Verification
194:interactions are satisfied. This is a case of
217:Design and Validation of Computer Protocols
210:Protocol Engineering, Advances in Computers
38:When the first experimental and commercial
281:
279:
256:
254:
174:Constructive methods for protocol design
89:
81:
276:
251:
236:P. Venkataram, S.S. Manvi, B.S. Babu,
348:
132:
26:. It uses many of the principles of
13:
238:Communication Protocol Engineering
231:Communication Protocol Engineering
14:
367:
269:See the series of conferences on
212:, Volume 29, 1989, Pages 79-195.
166:for protocol verification, and
333:
324:
315:
306:
297:
288:
263:
1:
244:
170:for entity implementations.
86:Layered protocol architecture
77:
7:
124:Test suite development for
10:
372:
233:, CRC Press, 2nd Ed. 2018.
33:
202:
58:, in particular for the
155:model-based development
24:communication protocols
219:, Prentice Hall, 1991.
95:
87:
144:Reachability analysis
93:
85:
356:Software engineering
224:Protocol Engineering
159:software engineering
140:formal specification
28:software engineering
20:Protocol engineering
196:supervisory control
126:conformance testing
44:distributed systems
273:(PSTV) since 1981.
96:
88:
72:UML state machines
56:OSI protocol stack
226:, Springer, 2012.
133:Methods and tools
40:computer networks
363:
340:
337:
331:
328:
322:
319:
313:
310:
304:
301:
295:
292:
286:
283:
274:
267:
261:
258:
371:
370:
366:
365:
364:
362:
361:
360:
346:
345:
344:
343:
338:
334:
329:
325:
320:
316:
311:
307:
302:
298:
293:
289:
284:
277:
268:
264:
259:
252:
247:
215:G.J. Holzmann,
205:
176:
135:
80:
60:transport layer
36:
17:
12:
11:
5:
369:
359:
358:
342:
341:
332:
323:
314:
305:
296:
287:
275:
262:
249:
248:
246:
243:
242:
241:
234:
227:
220:
213:
204:
201:
200:
199:
191:
188:
184:
175:
172:
164:model checking
148:model checking
134:
131:
130:
129:
122:
117:
116:
113:
110:
107:
104:
79:
76:
35:
32:
15:
9:
6:
4:
3:
2:
368:
357:
354:
353:
351:
336:
327:
318:
309:
300:
291:
282:
280:
272:
266:
257:
255:
250:
239:
235:
232:
228:
225:
221:
218:
214:
211:
208:Ming T. Liu,
207:
206:
197:
192:
189:
185:
182:
181:
180:
171:
169:
168:agile methods
165:
160:
156:
151:
149:
145:
141:
127:
123:
119:
118:
114:
111:
108:
105:
101:
100:
99:
92:
84:
75:
73:
69:
63:
61:
57:
51:
49:
45:
41:
31:
29:
25:
21:
335:
326:
317:
308:
299:
290:
265:
237:
230:
229:M. Popovic,
223:
216:
209:
177:
152:
136:
97:
64:
52:
37:
19:
18:
245:References
222:H. König,
78:Principles
48:OSI model
350:Category
240:, 2014.
187:entity.
121:entity.
34:History
103:(n-1).
203:Books
74:.
68:SDL
352::
278:^
253:^
62:.
198:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
