286:
278:
270:
377:, which means that two messages are received and their order is not defined (which is often the case if they come from different partners). Many of these design flaws disappear when multiple queues or reception pools are used. With the systematic use of reception pools, reachability analysis should check for partial deadlocks and messages remaining forever in the pool (without being consumed by the entity)
211:. In the simplest case, the medium between two entities is modeled by two FIFO queues in opposite directions, which contain the messages in transit (that are sent, but not yet consumed). Reachability analysis considers the possible behavior of the distributed system by analyzing all possible sequences of state transitions of the entities, and the corresponding global states reached.
215:
entities. However, in many cases this transition graph is unbounded and can not be explored completely. The transition graph can be used for checking general design flaws of the protocol (see below), but also for verifying that the sequences of service interactions by the entities correspond to the requirements given by the global service specification of the system.
214:
The result of reachability analysis is a global state transition graph (also called reachability graph) which shows all global states of the distributed system that are reachable from the initial global state, and all possible sequences of send, consume and service interactions performed by the local
404:
A practical issue of reachability analysis is the so-called ″state space explosion″. If the two entities of a protocol have 100 states each, and the medium may include 10 types of messages, up to two in each direction, then the number of global states in the reachability graph is bound by the number
335:
is normally not reliable and allows for erroneous reception and message loss (modeled as a state transition of the medium). Protocols using the
Internet IP service should also deal with the possibility of out-of-order delivery. Higher-level protocols normally use a session-oriented Transport service
313:
The third diagram shows the result of the reachability analysis for this protocol in the form of a global state machine. Each global state has four components: the state of protocol entity A (left), the state of the entity B (right) and the messages in transit in the middle (upper part: from A to B;
309:
with one another, as shown in the first diagram. The protocol is defined by the behavior of the two entities, which is given in the second diagram in the form of two state machines. Here the symbol "!" means sending a message, and "?" means consuming a received message. The initial states are the
368:
Each entity has a single pool where received messages are stored until they are consumed. Here the entity has the power to decide, depending on its state, which type of message should be consumed next (and wait for a message if none has been received yet), or possibly consume one from a set of
248:
An entity is in a deadlocked state if it waits for the consumption of a message and the system is in a global state where such a message is not in transit and will never be sent in any global state that can be reached in the future. Such a non-local property can be verified by performing
330:
The design of a protocol has to be adapted to the properties of the underlying communication medium, to the possibility that the communication partner fails, and to the mechanism used by an entity to select the next message for consumption. The communication medium for protocols at the
317:
One sees that this example has a bounded global state space - the maximum number of messages that may be in transit at the same time is two. This protocol has a global deadlock, which is the state . If one removes the transition of A in state 2 for consuming message
226:
The global state transition graph is bounded if the number of messages that may be in transit is bounded and the number states of all entities is bounded. The question whether the number of messages remains bounded in the case of finite state entities is in general
259:
An entity has an unspecified reception if the next message to be consumed is not expected by the behavior specification of the entity in its current state. The absence of this condition can be verified by checking all states in the reachability
50:
For reachability analysis, the local entities are modeled by their states and transitions. An entity changes state when it sends a message, consumes a received message, or performs an interaction at its local service interface. The global state
26:
in the particular context of distributed systems. It is used to determine which global states can be reached by a distributed system which consists of a certain number of local entities that communicated by the exchange of messages.
405:
100 x 100 x (10 x 10) x (10 x 10) which is 100 million. Therefore a number of tools have been developed to automatically perform reachability analysis and model checking on the reachability graph. We mention only two examples: The
241:
The system is in a global deadlock if all entities wait for the consumption of a message and no message is in transit. Absence of global deadlocks can be verified by checking that no state in the reachability graph is a global
347:
Different assumptions have been made about whether an entity can select a particular message for consumption when several messages have arrived and are ready for consumption. The basic models are the following:
361:
Each entity has multiple FIFO queues, one for each communicating partner. Here the entity has the possibility to decide, depending on its state, from which queue (or queues) the next input message should be
147:
393:). However, this model is not powerful enough to model message parameters and local variables. Therefore often so-called extended FSM models are used, such as supported by languages like
373:
The original paper identifying the problem of unspecified receptions, and much of the subsequent work, assumed a single input queue. Sometimes, unspecified receptions are introduced by a
355:
Each entity has a single FIFO queue where incoming messages are stored until they are consumed. Here the entity has no selection power and has to consume the first message in the queue.
314:
lower part: from B to A). Each transition of this global state machine corresponds to one transition of protocol entity A or entity B. The initial state is (no messages in transit).
594:
C. Fournet, T. Hoare, S. K. Rajamani, and J. Rehof : Stuck-free
Conformance, Proc. 16th Intl. Conf. on Computer Aided Verification (CAV’04), LNCS, vol. 3114, Springer, 2004
563:
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 )
410:
289:
This diagram shows a state machine model of the global system consisting of the two protocol entities and two FIFO channels used for the exchange of messages between them.
47:
and, under certain assumptions, provides as service the correct data delivery without loss nor duplication, despite the occasional presence of message corruption or loss.
585:
M.F. Al-hammouri and G.v. Bochmann : Realizability of service specifications, Proc. System
Analysis and Modelling (SAM) conference 2018, Copenhagen, LNCS, Springer
540:
209:
43:
using finite-state modeling of the protocol entities, and also pointed out that a similar protocol described earlier had a design flaw. This protocol belongs to the
174:
340:, one often takes into account the possibility that some entity fails completely, which is normally detected (like a loss of message in the medium) by a
573:
394:
489:
K.A. Bartlett, R.A. Scantlebury and P.T. Wilkinson, A note on reliable full-duplex transmission over half- duplex links, C.ACM 12, 260 (1969).
437:
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.
285:
390:
336:
which means that the medium provides reliable FIFO transmission of messages between any pair of entities. However, in the analysis of
610:
576:
can be used to indicate that certain types of messages should not be consumed in the current state, but saved for future processing.
231:. One usually truncates the exploration of the transition graph when the number of messages in transit reaches a given threshold.
615:
277:
54:
458:
Bochmann, G.v. "Finite State
Description of Communication Protocols, Computer Networks, Vol. 2 (1978), pp. 361-372".
281:
The diagram shows two finite state machines that define the dynamic behavior of the respective protocol entities.
40:
422:
36:
463:
337:
386:
23:
551:
M.G.Gouda, E.G.Manning, Y.T.Yu: On the progress of communication between two finite state machines,
341:
228:
406:
398:
35:
Reachability analysis was introduced in a paper of 1978 for the analysis and verification of
510:
179:
152:
476:
293:
As an example, we consider the system of two protocol entities that exchange the messages
374:
250:
604:
431:
39:. This paper was inspired by a paper by Bartlett et al. of 1968 which presented the
269:
507:
Note: The corruption or loss of a message is modeled as a state transition of the
401:. Unfortunately, reachability analysis becomes much more complex for such models.
552:
273:
The diagram shows two protocol entities and the messages exchanged between them.
332:
44:
16:
Solution to the reachability problem in distributed systems (computer science)
498:
Note: In the case of protocol analysis, there are normally only two entities.
427:
322:, there will be an unspecified reception in the global states and .
389:(FSM) to model the behavior of the distributed entities (see also
284:
276:
268:
176:(i=1, ... n) of the entities and the state of the communication
428:
Gerald
Holzmann: Design and Validation of Computer Protocols
149:
of a system with n entities is determined by the states
513:
182:
155:
57:
344:
mechanism when an expected message does not arrive.
369:
message types (in order to deal with alternatives).
534:
411:construction and analysis of distributed processes
203:
168:
141:
142:{\displaystyle s=(s_{1},s_{2},...,s_{n},medium)}
8:
385:Most of the work on protocol modeling use
512:
181:
160:
154:
109:
84:
71:
56:
453:
451:
447:
472:
461:
7:
391:Communicating finite-state machines
14:
234:The following are design flaws:
136:
64:
1:
572:Note: The SAVE construct of
632:
253:on the reachability graph.
611:Communications protocols
41:alternating bit protocol
423:Communication protocols
37:communication protocols
536:
535:{\displaystyle medium}
471:Cite journal requires
409:and a toolbox for the
338:distributed algorithms
290:
282:
274:
257:Unspecified reception:
205:
204:{\displaystyle medium}
170:
143:
616:Theory of computation
537:
387:finite-state machines
288:
280:
272:
206:
171:
169:{\displaystyle s_{i}}
144:
22:is a solution to the
20:Reachability analysis
511:
442:References and notes
326:Message transmission
180:
153:
55:
24:reachability problem
353:Single input queue:
219:Protocol properties
532:
407:SPIN model checker
399:UML state machines
291:
283:
275:
246:Partial deadlocks:
201:
166:
139:
623:
595:
592:
586:
583:
577:
570:
564:
561:
555:
549:
543:
541:
539:
538:
533:
505:
499:
496:
490:
487:
481:
480:
474:
469:
467:
459:
455:
381:Practical issues
359:Multiple queues:
239:Global deadlock:
210:
208:
207:
202:
175:
173:
172:
167:
165:
164:
148:
146:
145:
140:
114:
113:
89:
88:
76:
75:
631:
630:
626:
625:
624:
622:
621:
620:
601:
600:
599:
598:
593:
589:
584:
580:
571:
567:
562:
558:
550:
546:
509:
508:
506:
502:
497:
493:
488:
484:
470:
460:
457:
456:
449:
444:
419:
417:Further reading
383:
366:Reception pool:
328:
267:
221:
178:
177:
156:
151:
150:
105:
80:
67:
53:
52:
33:
17:
12:
11:
5:
629:
627:
619:
618:
613:
603:
602:
597:
596:
587:
578:
565:
556:
544:
531:
528:
525:
522:
519:
516:
500:
491:
482:
473:|journal=
446:
445:
443:
440:
439:
438:
435:
425:
418:
415:
382:
379:
375:race condition
371:
370:
363:
356:
327:
324:
266:
263:
262:
261:
254:
251:model checking
243:
220:
217:
200:
197:
194:
191:
188:
185:
163:
159:
138:
135:
132:
129:
126:
123:
120:
117:
112:
108:
104:
101:
98:
95:
92:
87:
83:
79:
74:
70:
66:
63:
60:
32:
29:
15:
13:
10:
9:
6:
4:
3:
2:
628:
617:
614:
612:
609:
608:
606:
591:
588:
582:
579:
575:
569:
566:
560:
557:
554:
548:
545:
529:
526:
523:
520:
517:
514:
504:
501:
495:
492:
486:
483:
478:
465:
454:
452:
448:
441:
436:
433:
432:Prentice Hall
429:
426:
424:
421:
420:
416:
414:
412:
408:
402:
400:
396:
392:
388:
380:
378:
376:
367:
364:
360:
357:
354:
351:
350:
349:
345:
343:
339:
334:
325:
323:
321:
315:
311:
308:
304:
300:
296:
287:
279:
271:
264:
258:
255:
252:
247:
244:
240:
237:
236:
235:
232:
230:
229:not decidable
225:
218:
216:
212:
198:
195:
192:
189:
186:
183:
161:
157:
133:
130:
127:
124:
121:
118:
115:
110:
106:
102:
99:
96:
93:
90:
85:
81:
77:
72:
68:
61:
58:
48:
46:
42:
38:
30:
28:
25:
21:
590:
581:
568:
559:
547:
503:
494:
485:
464:cite journal
403:
384:
372:
365:
358:
352:
346:
329:
319:
316:
312:
310:states "1".
306:
302:
298:
294:
292:
256:
245:
238:
233:
224:Boundedness:
223:
222:
213:
49:
34:
19:
18:
605:Categories
333:Link level
265:An example
45:Link layer
362:consumed.
242:deadlock.
31:Overview
434:, 1991.
342:timeout
260:graph.
477:help
305:and
574:SDL
553:doi
397:or
395:SDL
607::
468::
466:}}
462:{{
450:^
430:,
413:.
320:mb
307:md
303:mc
301:,
299:mb
297:,
295:ma
542:.
530:m
527:u
524:i
521:d
518:e
515:m
479:)
475:(
199:m
196:u
193:i
190:d
187:e
184:m
162:i
158:s
137:)
134:m
131:u
128:i
125:d
122:e
119:m
116:,
111:n
107:s
103:,
100:.
97:.
94:.
91:,
86:2
82:s
78:,
73:1
69:s
65:(
62:=
59:s
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
