*** Real-Time Maude 2.1 specification of AER/NCA protocol suite *** This file should be read when the RTT protocol is to be executed *** by itself. It reads the appropriate files and defines some *** initial states. It also contains some prototyping and analysis *** commands, commented away. in AER-prelude.rtmaude in AER-commonclasses.rtmaude in AER-shared-msgs.rtmaude in rtt.rtmaude (tomod AER-RTT1 is including AER-RTT . ops RTTstate1 RTTstate2 : Nat -> GlobalSystem . --- Parameterized by the random number generator's initial "seed" value eq RTTstate1(N:Nat) = ( { startRTT('a) < 'a : RTTsenderAlone | clock : 0, sourceRTT : 0, children : 'b 'c, maxDownRTT : INF, maxDownRTTSetTime : 0, maxRecentDownRTT : 0 > < 'b : RTTrepairserverAlone | clock : 0, sourceRTT : INF, children : 'd, maxDownRTT : INF, maxDownRTTSetTime : 0, maxRecentDownRTT : 0, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF > < 'c : RTTrepairserverAlone | clock : 0, sourceRTT : INF, children : 'f, maxDownRTT : INF, maxDownRTTSetTime : 0, maxRecentDownRTT : 0, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF > < 'd : RTTreceiverAlone | clock : 0, sourceRTT : INF, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF > < 'f : RTTrepairserverAlone | clock : 0, sourceRTT : INF, children : 'i, maxDownRTT : INF, maxDownRTTSetTime : 0, maxRecentDownRTT : 0, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF > < 'i : RTTreceiverAlone | clock : 0, sourceRTT : INF, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF > < 'random : RandomNGen | seed : N:Nat > < 'ac : Link | up : 'a, down : 'c, bound : 6, propDelay : 14, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'ab : Link | up : 'a, down : 'b, bound : 18, propDelay : 35, linkSpeed : 2, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'bd : Link | up : 'b, down : 'd, bound : 14, propDelay : 10, linkSpeed : 8, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'cf : Link | up : 'c, down : 'f, bound : 11, propDelay : 27, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'fi : Link | up : 'f, down : 'i, bound : 12, propDelay : 5, linkSpeed : 10, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > }) . *** The next system is one proposed by Mark Keaton in Boston: eq RTTstate2(N:Nat) = ({ startRTT('a) < 'a : RTTsenderAlone | clock : 0, sourceRTT : 0, children : 'b 'c, maxDownRTT : INF, maxDownRTTSetTime : 0, maxRecentDownRTT : 0 > < 'b : RTTreceiverAlone | clock : 0, sourceRTT : INF, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF > < 'c : RTTrepairserverAlone | clock : 0, sourceRTT : INF, children : 'd 'e, maxDownRTT : INF, maxDownRTTSetTime : 0, maxRecentDownRTT : 0, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF > < 'd : RTTrepairserverAlone | clock : 0, sourceRTT : INF, children : 'f 'g, maxDownRTT : INF, maxDownRTTSetTime : 0, maxRecentDownRTT : 0, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF > < 'e : RTTreceiverAlone | clock : 0, sourceRTT : INF, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF > < 'f : RTTreceiverAlone | clock : 0, sourceRTT : INF, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF > < 'g : RTTreceiverAlone | clock : 0, sourceRTT : INF, repairserver : noOid, resendInterval : 200, maxUpRTT : INF, myUpRTT : INF, getRTTResendTimer : INF > < 'random : RandomNGen | seed : N:Nat > < 'ab : Link | up : 'a, down : 'b, bound : 5, propDelay : 21, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'ac : Link | up : 'a, down : 'c, bound : 21, propDelay : 28, linkSpeed : 3, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'cd : Link | up : 'c, down : 'd, bound : 9, propDelay : 23, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'ce : Link | up : 'c, down : 'e, bound : 4, propDelay : 17, linkSpeed : 1, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'df : Link | up : 'd, down : 'f, bound : 12, propDelay : 5, linkSpeed : 10, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 > < 'dg : Link | up : 'd, down : 'g, bound : 12, propDelay : 5, linkSpeed : 10, downMsgs : nil, downSize : 0, upMsgs : nil, upSize : 0 >}) . endtom) --- ----------------------------------------------------------- --- FORMAL ANALYSIS --- ----------------------------------------------------------- --- [remember that we use a "maximal" time sampling strategy, declared --- earlier.] --- Prototyping: --- (trew RTTstate1(1) in time <= 1000 .) --- (trew RTTstate2(1) in time <= 1000 .) --- Find EARLIEST time in which the correct sourceRTT and maxUpRTT values --- can be found: ***( --- commented away (find earliest RTTstate2(1) =>* {< 'b : RTTreceiverAlone | sourceRTT : 44, maxUpRTT : 58, ATTS1:AttributeSet > < 'c : RTTrepairserverAlone | sourceRTT : 58, maxUpRTT : 58, ATTS2:AttributeSet > < 'd : RTTrepairserverAlone | sourceRTT : 106, maxUpRTT : 48, ATTS3:AttributeSet > < 'e : RTTreceiverAlone | sourceRTT : 94, maxUpRTT : 48, ATTS4:AttributeSet > < 'f : RTTreceiverAlone | sourceRTT : 118, maxUpRTT : 12, ATTS5:AttributeSet > < 'g : RTTreceiverAlone | sourceRTT : 118, maxUpRTT : 12, ATTS6:AttributeSet > C:Configuration} .) )*** --- What is the longest time needed, in the worst case, to find the desired --- sourceRTT and maxUpRTT values? ***( --- commented away (find latest RTTstate2(1) =>* {< 'b : RTTreceiverAlone | sourceRTT : 44, maxUpRTT : 58, ATTS1:AttributeSet > < 'c : RTTrepairserverAlone | sourceRTT : 58, maxUpRTT : 58, ATTS2:AttributeSet > < 'd : RTTrepairserverAlone | sourceRTT : 106, maxUpRTT : 48, ATTS3:AttributeSet > < 'e : RTTreceiverAlone | sourceRTT : 94, maxUpRTT : 48, ATTS4:AttributeSet > < 'f : RTTreceiverAlone | sourceRTT : 118, maxUpRTT : 12, ATTS5:AttributeSet > < 'g : RTTreceiverAlone | sourceRTT : 118, maxUpRTT : 12, ATTS6:AttributeSet > C:Configuration} in time < 5000 .) )*** --- Is it true, that, within time 1000, once the correct values have been --- found, that they will not be changed? ***( Takes long time (2 minutes): (check RTTstate2(1) |= {C:Configuration} untilStable {< 'b : RTTreceiverAlone | sourceRTT : 44, maxUpRTT : 58, ATTS1:AttributeSet > < 'c : RTTrepairserverAlone | sourceRTT : 58, maxUpRTT : 58, ATTS2:AttributeSet > < 'd : RTTrepairserverAlone | sourceRTT : 106, maxUpRTT : 48, ATTS3:AttributeSet > < 'e : RTTreceiverAlone | sourceRTT : 94, maxUpRTT : 48, ATTS4:AttributeSet > < 'f : RTTreceiverAlone | sourceRTT : 118, maxUpRTT : 12, ATTS5:AttributeSet > < 'g : RTTreceiverAlone | sourceRTT : 118, maxUpRTT : 12, ATTS6:AttributeSet > C:Configuration} in time < 1000 .) )*** --- ------------------------------------- --- Temporal logic analysis --- ------------------------------------- --- Must first define the proposition CORRECT-RTT-VALUES: (tomod MODEL-CHECK-RTT is protecting AER-RTT1 . including TIMED-MODEL-CHECKER . op CORRECT-RTT-VALUES : -> Prop . eq {< 'b : RTTreceiverAlone | sourceRTT : 44, maxUpRTT : 58 > < 'c : RTTrepairserverAlone | sourceRTT : 58, maxUpRTT : 58 > < 'd : RTTrepairserverAlone | sourceRTT : 106, maxUpRTT : 48 > < 'e : RTTreceiverAlone | sourceRTT : 94, maxUpRTT : 48 > < 'f : RTTreceiverAlone | sourceRTT : 118, maxUpRTT : 12 > < 'g : RTTreceiverAlone | sourceRTT : 118, maxUpRTT : 12 > C:Configuration} |= CORRECT-RTT-VALUES = true . endtom) --- The correct values always found within time 300: --- (mc RTTstate2(1) |=t <> CORRECT-RTT-VALUES in time <= 300 .) --- Stability. First of all, the values must be found, and once found, --- they should not change, within time 200. This should correspond --- to our "untilStable" check above. Notice that restricting --- the property to time 150 will give a counterexample. ***( (mc RTTstate2(1) |=t (<> CORRECT-RTT-VALUES) /\ (CORRECT-RTT-VALUES => [] CORRECT-RTT-VALUES) in time <= 1000 .) )***