*** Real-Time Maude 2.1 specification of AER/NCA protocol suite *** By Peter Csaba Olveczky *** File "nomX.rtmaude", for execution/analysis of the NOMINEE component *** Imports all the necessary file and defines som initial states *** which allows executing the NOM separately. *** Includes some analysis commands, which are commented away. in AER-prelude.rtmaude *** starts Real-Time Maude and reads *** some basic modules in AER-commonclasses.rtmaude in AER-shared-atts.rtmaude in AER-shared-msgs.rtmaude in EfficientWindow.rtmaude *** reads data type Window for sliding windows in nom.rtmaude (tomod NCA-NOM1 is protecting NCA-NOM . var N : Nat . op NOMstate1 : Nat -> GlobalSystem . eq NOMstate1(N) = ({ startNOM('a) < 'a : NOMsenderAlone | clock : 0, children : 'b 'c, NAMTimer : INF, csmLPE : noRat, csmRTT : 0, csmSetTime : 0, csmNominee : noOid > < 'b : NOMrepairserverAlone | clock : 0, repairserver : noOid, children : 'd, csmLPE : noRat, csmRTT : 0, csmAddress : noOid, csmSetTime : 0, csmTimer : INF > < 'c : NOMrepairserverAlone | clock : 0, children : 'f, repairserver : noOid, csmLPE : noRat, csmRTT : 0, csmAddress : noOid, csmSetTime : 0, csmTimer : INF > < 'd : NOMreceiverAlone | sourceRTT : 90, repairserver : noOid, isNominee : false, msgWindow : initWindow(4), csmTimer : INF > < 'f : NOMrepairserverAlone | clock : 0, children : 'i, repairserver : noOid, csmLPE : noRat, csmRTT : 0, csmAddress : noOid, csmSetTime : 0, csmTimer : INF > < 'i : NOMreceiverAlone | sourceRTT : 96, repairserver : noOid, isNominee : false, msgWindow : initWindow(4), csmTimer : INF > < 'random : RandomNGen | seed : N > < '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 > < 'env : Env | msgsFromEnv : dly(dataPacket(1, 0) from 'b to 'd, 5001) dly(dataPacket(2, 0) from 'b to 'd, 5002) dly(dataPacket(4, 0) from 'b to 'd, 5004) dly(dataPacket(9, 0) from 'b to 'd, 10000) dly(dataPacket(4, 0) from 'f to 'i, 5002) dly(dataPacket(5, 0) from 'f to 'i, 10000) dly(dataPacket(7, 0) from 'f to 'i, 10004) > }) . *** In the above, at time 5004, d has received 3 msg in its window (75%) *** and i has one msg in its window (25%). At time 10004, d has 25% *** and i has 50%. Alas, i should be the nominee in time (5004, 10003), and *** d thereafter. op NOMstate2 : Nat -> GlobalSystem . *** Mark Keaton's initial state. eq NOMstate2(N) = ({ startNOM('a) < 'a : NOMsenderAlone | clock : 0, children : 'b 'c, NAMTimer : INF, csmLPE : noRat, csmRTT : 0, csmSetTime : 0, csmNominee : noOid > < 'b : NOMreceiverAlone | sourceRTT : 44, repairserver : noOid, isNominee : false, msgWindow : initWindow(4), csmTimer : INF > < 'c : NOMrepairserverAlone | clock : 0, children : 'd 'e, repairserver : noOid, csmLPE : noRat, csmRTT : 0, csmAddress : noOid, csmSetTime : 0, csmTimer : INF > < 'd : NOMrepairserverAlone | clock : 0, children : 'f 'g, repairserver : noOid, csmLPE : noRat, csmRTT : 0, csmAddress : noOid, csmSetTime : 0, csmTimer : INF > < 'e : NOMreceiverAlone | sourceRTT : 94, repairserver : noOid, isNominee : false, msgWindow : initWindow(4), csmTimer : INF > < 'f : NOMreceiverAlone | sourceRTT : 118, repairserver : noOid, isNominee : false, msgWindow : initWindow(4), csmTimer : INF > < 'g : NOMreceiverAlone | sourceRTT : 118, repairserver : noOid, isNominee : false, msgWindow : initWindow(4), csmTimer : INF > < 'random : RandomNGen | seed : N > < '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 > < 'env : Env | msgsFromEnv : dly(dataPacket(1, 1) from 'a to 'b, 5001) dly(dataPacket(4, 1) from 'a to 'b, 5004) dly(dataPacket(2, 1) from 'd to 'f, 14996) dly(dataPacket(3, 1) from 'd to 'f, 14999) dly(dataPacket(4, 1) from 'd to 'f, 15031) dly(dataPacket(4, 1) from 'd to 'g, 5002) dly(dataPacket(5, 1) from 'd to 'g, 15000) dly(dataPacket(6, 1) from 'd to 'g, 15004) dly(dataPacket(1, 1) from 'c to 'e, 5003) dly(dataPacket(2, 1) from 'c to 'e, 5018) dly(dataPacket(16, 1) from 'c to 'e, 15001) > }) . endtom) --- In NOMstate2, in the beginning, and up to around time --- 15000, either f or g shopuld be the nominee. After that, --- e should be the nominee. --- Rewriting, check the above properties for SOME behavior: --- -------------------------------------------------------- --- (trew NOMstate2(1) in time <= 5000 .) --- (trew NOMstate2(1) in time <= 14500 .) --- (trew NOMstate2(1) in time <= 20000 .) --- Search analysis: --- ------------------ --- Our rewrite analysis found that 'f is selected the nominee --- in the beginning. It should equally well be 'g. Is it --- possible to select 'g to be the nominee? ***( (tsearch [1] NOMstate2(1) =>* {< 'g : NOMreceiverAlone | isNominee : true, ATTS:AttributeSet > C:Configuration} in time <= 5000 .) )*** --- No other receiver than 'f and 'g can be the nominee until --- time 15000: ***( (tsearch [1] NOMstate2(1) =>* {< 'a : NOMsenderAlone | csmNominee : O:Oid, ATTS:AttributeSet > C:Configuration} such that O:Oid =/= 'f /\ O:Oid =/= 'g in time <= 15000 .) )*** --- SOME nominee is always found within time 500: ***( (find latest NOMstate2(1) =>* {< O:Oid : NOMreceiverAlone | isNominee : true, ATTS:AttributeSet > C:Configuration} with no time limit .) )*** --- Receiver 'e should not be the nominee before time 15000: ***( (find earliest NOMstate2(1) =>* {< 'e : NOMreceiverAlone | isNominee : true, ATTS:AttributeSet > C:Configuration} .) )*** --- Eventuelly, 'e must be the nominee: ***( (find latest NOMstate2(1) =>* {< 'e : NOMreceiverAlone | isNominee : true, ATTS:AttributeSet > C:Configuration} with no time limit .) )*** --- Once 'e is found to be the nominee, it should remain so: ***( (check NOMstate2(1) |= {C:Configuration} untilStable {< 'e : NOMreceiverAlone | isNominee : true, ATTS:AttributeSet > C:Configuration} in time <= 30000 .) )*** --- We have already showed that a nominee is always found within time 500. --- However, this property is not stable, and we may once again be --- without nominee: ***( (check NOMstate2(1) |= {C:Configuration} untilStable {< O:Oid : NOMreceiverAlone | isNominee : true, ATTS:AttributeSet > C:Configuration} with no time limit .) )*** --- Temporal logic model checking. --- ----------------------------- --- We first analyze the main property that --- in the beginning, there is no nominee, --- then, either 'f or 'g is the nominee, as so it stays, --- until there is a message for 'e saying that it is the nominee, --- and then 'e becomes the nominee, and that lasts forever. --- The following module defines the propositions --- nomineeExists, nomineeIs, and becomingNominee: (tomod MODEL-CHECK-NCA is including TIMED-MODEL-CHECKER . protecting NCA-NOM1 . ops nomineeExists : -> Prop . eq {< O:Oid : NOMreceiverAlone | isNominee : true > C:Configuration} |= nomineeExists = true . ops nomineeIs becomingNominee : Oid -> Prop . eq {< O:Oid : NOMreceiverAlone | isNominee : true > C:Configuration} |= nomineeIs(O:Oid) = true . eq {(NAMPacket(true) from O:Oid to O':Oid) C:Configuration} |= becomingNominee(O':Oid) = true . endtom) --- Nominee always found withing time 500: --- (mc NOMstate2(1) |=t <> nomineeExists in time <= 500 .) --- Eventually, e must be the nominee: --- (mc NOMstate2(1) |=u <> nomineeIs('e) .) --- The total behavior should be as follows: ***( (mc NOMstate2(1) |=t ~ nomineeExists U ((nomineeIs('f) \/ nomineeIs('g)) /\ ((nomineeIs('f) -> (nomineeIs('f) U (becomingNominee('e) U ([] nomineeIs('e))))) /\ (nomineeIs('g) -> (nomineeIs('g) U (becomingNominee('e) U ([] nomineeIs('e))))))) in time <= 50000 .) )*** *** Clocked model checking. The above behavior should hold, but *** in addition, f or g should be the nominee before time 500 and *** not after 20000, and e should not be the nominee before time 15300. (tomod MODEL-CHECK-CLOCKED-NOM is protecting MODEL-CHECK-NCA . ops nomineeIsBefore nomineeIsAfter : Oid Time -> Prop . eq {< O:Oid : NOMreceiverAlone | isNominee : true > C:Configuration} in time R:Time |= nomineeIsBefore(O:Oid, R':Time) = R:Time <= R':Time . eq {< O:Oid : NOMreceiverAlone | isNominee : true > C:Configuration} in time R:Time |= nomineeIsAfter(O:Oid, R':Time) = R':Time <= R:Time . endtom) --- This is the main property: ***( (mc NOMstate2(1) |=t ~ nomineeExists U ((nomineeIsBefore('f, 500) \/ nomineeIsBefore('g, 500)) /\ ((nomineeIsBefore('f, 500) -> (nomineeIsBefore('f, 20000) U (becomingNominee('e) U ([] nomineeIsAfter('e, 15300))))) /\ (nomineeIsBefore('g, 500) -> (nomineeIsBefore('g, 20000) U (becomingNominee('e) U ([] nomineeIsAfter('e, 15300))))))) in time <= 50000 .) )*** *** The following should give false ... and a counterexample ... *** ... which it also does!! ***( (mc NOMstate2(1) |=t ~ nomineeExists U ((nomineeIsBefore('f, 500) \/ nomineeIsBefore('g, 500)) /\ ((nomineeIsBefore('f, 500) -> (nomineeIsBefore('f, 20000) U (becomingNominee('e) U ([] nomineeIsAfter('e, 25300))))) /\ (nomineeIsBefore('g, 500) -> (nomineeIsBefore('g, 20000) U (becomingNominee('e) U ([] nomineeIsAfter('e, 15300))))))) in time < 30000 .) )***