RFC904 - Exterior Gateway Protocol formal specification(2)

时间:2005-02-11 来源: 作者: 点击:
RFC-888 Minor functional enhancements are necessary in the RFC-888 messageformats to support certain features assumed of the state-machine model,in particular the capability to request a neighbor to
  RFC-888 Minor functional enhancements are necessary in the RFC-888 message formats to support certain features assumed of the state-machine model, in particular the capability to request a neighbor to suppress Hello commands. In addition, the model suggests a mapping between its states and certain status and error indications which clarifies and generalizes the interpretation. All of the header fields except the Status field (called the Information field at some places in RFC-888) remain unchanged. The following table summarizes the suggested format changes in the Status field for the various messages by (Type, Code) class. Class Messages Status Codes ------------------------------------------------------------------- 3,0 Request 0 unspecified 3,1 Confirm 1 active mode 3,2 Refuse 2 passive mode 3,3 Cease 3 insufficient resources 3,4 Cease-ack 4 administratively prohibited 5 going down 6 parameter problem 5,0 Hello 0 indeterminate 5,1 I-H-U 1 Up state 2,0 Poll 2 Down state 1,0 Update 128 unsolicited message bit 8,0 Error The changes from RFC-888 are as follows: 1. The status codes have been combined in two classes, one for those messages involved in starting and stopping the protocol and the other for those messages involved in maintaining the protocol and exchanging reachability information. Some messages of either class may not use all the status codes assigned. 2. The status codes for the Request and Confirm indicate whether the sender can operate in active or passive mode. In RFC-888 this field must be zero; however, RFC-888 does not specify any mechanism to decide how the neighbors poll each other. 3. The status codes for the Cease, Refuse and Cease-ack have the same interpretation. This provides a clear and unambiguous indication when the protocol is terminated due to an unusual situation, for instance if the NOC dynamically repartitions the ARPANET. The assigned codes are not consistent with RFC-888, since the codes for the Refuse and Cease were assigned conflicting values; however, the differences are minor and should cause no significant problems. Exterior Gateway Protocol Formal Specification Page 27 D.L. Mills 4. The status codes for the Hello, I-H-U, Poll, Update and Error have the same interpretation. Codes 0 through 2 are mutually exclusive and are chosen solely on the basis of the state of the sender. In the case of the Update (and possibly Error) one of these codes can be combined with the "unsolicited bit," which corresponds to code 128. In RFC-888 this field is unused for the Poll and Error and may contain only zero or 128 for the Update, so that the default case is to assume that reciprocal reachability cannot be determined by these messages. 5. Some of the reachability codes defined in RFC-888 have been removed as not applicable. Exterior Gateway Protocol Formal Specification Page 28 D.L. Mills Appendix C. Reachability Analysis The following table shows the state transitions which can occur in a system of two neighboring EGP gateways. Besides being useful in the design and verification of the protocol, the table is useful for implementation and testing. The system of two neighboring EGP gateways is modelled as a finite-state automaton constructed as the cartesian product of two state machines as defined above. Each state of this machine is represented as [i,j], where i and j are states of the original machine. Each line of the table shows one state transition of the machine in the form: [i1,j1] -> [i2,j2] E A which specifies the machine in state [i1,j1] presented with event E transitions to state [i2,j2] and generates action A. Multiple actions are separated by the "/" symbol. The special symbol "*" represents the set of lines where all "*"s in the line take on the (same) values 0 - 4 in turn. The table shows only those transitions which can occur as the result of events arriving at one of the two neighbors. The full table includes a duplicate set of lines for the other neighbor as well, with each line derived from a line of the table below using the transformation: [i1,j1] -> [i2,j2] E A => [j1,i1] -> [j2,i2] E A State State Event Actions --------------------------------------------------- [*,4] -> [0,4] Cease Cease-ack [0,1] -> [2,1] Request Confirm/Hello/Up/t1 [0,1] -> [0,1] Request Refuse [0,*] -> [1,*] Start Request/t1 [1,1] -> [2,1] Request Confirm/Hello/Up/t1 [1,2] -> [2,2] Confirm Hello/Up/t1 [1,3] -> [2,3] Confirm Hello/Up/t1 [1,0] -> [0,0] Refuse Null [1,*] -> [1,*] Start Request/r1 [1,*] -> [0,*] Stop Null [1,*] -> [1,*] t1 Request/t1 [2,1] -> [3,1] Up Down/Hello/Poll/t1/t2 [2,1] -> [2,1] Request Confirm/Hello/Up/t1 [2,2] -> [2,2] Hello I-H-U [2,3] -> [2,3] Hello I-H-U [2,2] -> [2,2] I-H-U Process Exterior Gateway Protocol Formal Specification Page 29 D.L. Mills [2,3] -> [2,3] I-H-U Process [2,*] -> [1,*] Start Request/r1 [2,*] -> [4,*] Stop Cease/t1 [2,1] -> [2,1] t1 Hello/t1 [2,2] -> [2,2] t1 Hello/t1 [2,3] -> [2,3] t1 Hello/t1 [3,1] -> [2,1] Down Null [3,2] -> [2,2] Down Null [3,3] -> [2,3] Down Null [3,1] -> [2,1] Request Confirm/Hello/Up/t1 [3,2] -> [3,2] Hello I-H-U [3,3] -> [3,3] Hello I-H-U [3,2] -> [3,2] I-H-U Process [3,3] -> [3,3] I-H-U Process [3,3] -> [3,3] Poll Update [3,3] -> [3,3] Update Process [3,*] -> [1,*] Start Request/r1 [3,*] -> [4,*] Stop Cease/t1 [3,1] -> [3,1] t1 Hello/t1 [3,2] -> [3,2] t1 Hello/t1 [3,3] -> [3,3] t1 Hello/t1 [3,1] -> [3,1] t2 Poll/t2 [3,2] -> [3,2] t2 Poll/t2 [3,3] -> [3,3] t2 Poll/t2 [4,1] -> [4,1] Request Cease [4,*] -> [0,*] Cease Cease-ack [4,0] -> [0,0] Cease-ack Null [4,*] -> [0,*] Stop Null [4,*] -> [4,*] t1 Cease/t1 In the state-machine model defined in this document all states of the above machine are reachable; however, some are reachable only in extreme cases when one neighbor crashes, for example. In the common case where only one of the neighbors initiates and terminates the protocol and neither one crashes, for example, not all states are reachable. Following is a matrix showing the states which can be reached in this case, where the neighbor that initiates and terminates the protocol is called the active gateway and the other the passive gateway. Exterior Gateway Protocol Formal Specification Page 30 D.L. Mills Passive Gateway Active 0 Idle 1 Aqsn 2 Down 3 Up 4 Cease Gateway +-----------+-----------+-----------+-----------+-----------+ 0 Idle |stable | | | |unstable | 1 Aqsn |unstable |unstable |unstable |unstable |unstable | 2 Down | | |stable |unstable | | 3 Up | | |unstable |stable | | 4 Cease |unstable |unstable |unstable |unstable |unstable | +-----------+-----------+-----------+-----------+-----------+ In the above matrix the blank entries represent unreachable states, while those marked unstable represent transient states which cannot persist for long, due to retransmission of Request and Hello messages, for example.
------分隔线----------------------------
顶一下
(0)
0%
踩一下
(0)
0%
------分隔线----------------------------
最新评论 查看所有评论
发表评论 查看所有评论
请自觉遵守互联网相关的政策法规,严禁发布色情、暴力、反动的言论。
评价:
表情:
用户名: 密码: 验证码:
推荐内容