------------------------------------------------------------------------------- -- PART 1: EQUIVALENCE CHECKING OF VERSIONS A AND B ------------------------------------------------------------------------------- (* The shell variable CAESAR_OPTIONS contains the options to pass to the CAESAR tool, which will generate the BCG graphs from LNT descriptions Option -monitor will open a window with real-time information about the BCG graph being generated. When a generation completes, you must press the "Done" button to continue the execution of this SVL script. *) % CAESAR_OPTIONS="-monitor" ------------------------------------------------------------------------------- (* We successively process "rel_rel_A.lnt" and "rel_rel_B.lnt" *) % for SPEC in "rel_rel_A" "rel_rel_B" % do (* The BCG graph corresponding to the LNT specification "$SPEC.lnt" is generated. Then, hiding is performed in order to obtain an abstract version of the protocol that only refers to the actions needed for verification. Concretely, all labels of the form "CRASH ..." and "GET !2 ..." are hidden. The resulting graph is minimized for branching bisimulation, and then stored in file "$SPEC.bcg". *) "$SPEC.bcg" = branching reduction of total hide "CRASH .*", "GET !2 .*" in generation of "$SPEC.lnt"; ------------------------------------------------------------------------------- (* Then, two causality properties, expressed as graphs stored in files "service_1.aut" and "service_2.aut", are checked. *) (* The BCG graph stored in file "$SPEC.bcg" is compared with respect to safety equivalence to the graph stored in file "service_1.aut". *) "diag_1_${SPEC}.seq" = safety comparison "$SPEC.bcg" == "service_1.aut"; ------------------------------------------------------------------------------- (* The BCG graph stored in file "$SPEC.bcg" is compared with respect to tau*.a equivalence to the graph stored in file "service_2.aut". *) "diag_2_${SPEC}.seq" = tau*.a comparison "$SPEC.bcg" == "service_2.aut"; % done ------------------------------------------------------------------------------- -- PART 2: MODEL CHECKING OF VERSION B ------------------------------------------------------------------------------- (* We now illustrate how version B of the rel/REL protocol can be verified compositionally. Version B of the rel/REL protocol is divided into five concurrent processes: Crash_Transmitter, Fail_Receiver (instances 1 and 2), and Receiver_Thread (instances 1 and 2). For each of these processes, the corresponding LTS is generated and reduced modulo strong equivalence. The five reduced LTSs are composed together using parallel and hiding operators. The parallel composition of the minimized processes is referred to as "rel_rel_B.exp". *) % DEFAULT_PROCESS_FILE="rel_rel_B.lnt" % CAESAR_OPTIONS="" "rel_rel_B.exp" = leaf strong reduction of hide R_T1, R_T2, R1, R2, DEPOSE1, DEPOSE2 in ( Crash_Transmitter [R_T1, R_T2] |[R_T1, R_T2]| ( ( Receiver_Thread [R_T1, R1, R2, DEPOSE1, GET, CRASH] (1 of ADR) |[R_T1, R1, R2, GET, CRASH, DEPOSE1]| Fail_Receiver [R_T1, R1, R2, GET, DEPOSE1, CRASH] (1 of ADR) ) |[R1, R2]| ( Receiver_Thread [R_T2, R2, R1, DEPOSE2, GET, CRASH] (2 of ADR) |[R_T2, R1, R2, GET, CRASH, DEPOSE2]| Fail_Receiver [R_T2, R2, R1, GET, DEPOSE2, CRASH] (2 of ADR) ) ) ); ------------------------------------------------------------------------------- (* Check for deadlocks *) "rel_rel_B_dead.seq" = deadlock of "rel_rel_B.exp"; % cat rel_rel_B_dead.seq | tr -d '\015' | grep -v '^$' ------------------------------------------------------------------------------- (* Check for livelocks *) "rel_rel_B_live.bcg" = livelock of "rel_rel_B.exp"; ------------------------------------------------------------------------------- (* * Reduce modulo branching bisimulation the LTS corresponding to "rel_rel_B.exp" * after hiding all labels of the form "GET !2 *" and "CRASH !*" *) "rel_rel_B_compo.bcg" = branching reduction of total hide "GET !2 .*", "CRASH .*" in "rel_rel_B.exp" ; ------------------------------------------------------------------------------- (* Compare the compositional LTS against the non-compositional one *) "rel_rel_service_1.seq" = branching comparison "rel_rel_B_compo.bcg" == "rel_rel_B.bcg"; ------------------------------------------------------------------------------- -- PART 3: COMPOSITIONAL VERIFICATION OF VERSION C ------------------------------------------------------------------------------- (* * Compositional Generation of the rel/REL protocol for three receiver nodes, * which is divided into four processes: * - Crash_Transmitter * - Receiver_Node (instance 1) * - Receiver_Node (instance 2) * - Receiver_Node (instance 3) * * Since the LTSs corresponding to the Receiver nodes are too large to * be generated from the LNT specification we adopt the following strategy: * * - The Crash Transmitter node is generated, and then reduced modulo strong * bisimulation (terminal reduction). * * - For each Receiver node, a restricted LTS is generated with respect to * the context constraints provided by its environment (the Transmitter * and the other Receiver nodes). Such "user-given" constraints are * described by the LNT specification "interface.lnt". These * restricted LTSs are then reduced modulo strong bisimulation. * * - Restricted LTS associated to each Receiver node are composed each other, * each parallel composition being also restricted with respect to the * context constraints provided by the Transmitter. The LTS resulting of * these compositions is then reduced modulo strong bisimulation. * * - Finally, the LTS associated to the Transmitter is generated, reduced * modulo strong bisimulation and composed with the one associated to the * Receiver nodes composition. Correcteness of the user-given constraints * is checked on this last composition. This results in an LTS named * "rel_rel_C.bcg". *) % DEFAULT_PROCESS_FILE="rel_rel_C.lnt" "crash_trans.bcg" = strong reduction of CRASH_TRANSMITTER; "rel_rel_C.bcg" = strong reduction of generation of leaf strong reduction of hide R_T1, R_T2, R_T3, R12, R13, R21, R23, R31, R32 in ( ( ( (Receiver_Node [R_T1, R21, R31, R12, R13, GET, CRASH] (1 of ADR) -||? "interface.lnt":INTERFACE [R_T1, R21, R31]) |[R12, R21, R13, R31]| ( (Receiver_Node [R_T2, R12, R32, R21, R23, GET, CRASH] (2 of ADR) -||? "interface.lnt":INTERFACE [R_T2, R12, R32]) |[R23, R32]| (Receiver_Node [R_T3, R13, R23, R31, R32, GET, CRASH] (3 of ADR) -||? "interface.lnt":INTERFACE [R_T3, R13, R23]) ) -|[R_T2, R_T3]| "crash_trans.bcg" ) -|[R_T1, R_T2, R_T3]| "crash_trans.bcg" ) |[R_T1, R_T2, R_T3]| "crash_trans.bcg" ); ------------------------------------------------------------------------------- (* * Verification of two requirements, named FIFO and ATOMICITY, which are * verified on "rel_rel_C.bcg". *) property FIFO "Messages are received in the order they have been sent." is (* * This property is verified by equivalence checking, using BISIMULATOR * to compare (modulo safety equivalence) the LTS "rel_rel_C.bcg" and * the LTS produced from the LNT specification "fifo.lnt", hiding * all labels but ones of the form "GET *". *) "fifo.seq" = safety comparison (hide all but GET in "rel_rel_C.bcg") == generation of "fifo.lnt"; expected TRUE end property ------------------------------------------------------------------------------- % DEFAULT_MCL_LIBRARIES="standard.mcl" property ATOMICITY "Whenever a functioning Receiver receives a message, then every other" "functioning Receiver eventually does." is (* This property is verified by model checking, first using a series * of 3x3 dataless formulas (checked by EVALUATOR) and then one single * value-passing formula (checked by EVALUATOR). Precisely, one verifies * that, for each message m, for each i in {1, 2, 3}, there exists no * sequence such that Receiver i gets the message and: * - neither another Receiver j gets the message, * - nor another Receiver j crashes, * - nor Receiver i crashes. *) -- dataless formula #1 for message 1 and receiver 1 "rel_rel_C.bcg" |= with evaluator [ (not ("CRASH !1" or "GET !1 !1"))* ] ( [ "GET !2 !1" ] INEVITABLE ('CRASH ![12]' or "GET !1 !1") and [ "GET !3 !1" ] INEVITABLE ('CRASH ![13]' or "GET !1 !1") ); expected TRUE; -- dataless formula #2 for message 1 and receiver 2 "rel_rel_C.bcg" |= with evaluator [ (not ("CRASH !2" or "GET !2 !1"))* ] ( [ "GET !1 !1" ] INEVITABLE ('CRASH ![21]' or "GET !2 !1") and [ "GET !3 !1" ] INEVITABLE ('CRASH ![23]' or "GET !2 !1") ); expected TRUE; -- dataless formula #3 for message 1 and receiver 3 "rel_rel_C.bcg" |= with evaluator [ (not ("CRASH !3" or "GET !3 !1"))* ] ( [ "GET !1 !1" ] INEVITABLE ('CRASH ![31]' or "GET !3 !1") and [ "GET !2 !1" ] INEVITABLE ('CRASH ![32]' or "GET !3 !1") ); expected TRUE; -- dataless formula #4 for message 2 and receiver 1 "rel_rel_C.bcg" |= with evaluator [ (not ("CRASH !1" or "GET !1 !2"))* ] ( [ "GET !2 !2" ] INEVITABLE ('CRASH ![12]' or "GET !1 !2") and [ "GET !3 !2" ] INEVITABLE ('CRASH ![13]' or "GET !1 !2") ); expected TRUE; -- dataless formula #5 for message 2 and receiver 2 "rel_rel_C.bcg" |= with evaluator [ (not ("CRASH !2" or "GET !2 !2"))* ] ( [ "GET !1 !2" ] INEVITABLE ('CRASH ![21]' or "GET !2 !2") and [ "GET !3 !2" ] INEVITABLE ('CRASH ![23]' or "GET !2 !2") ); expected TRUE; -- dataless formula #6 for message 2 and receiver 3 "rel_rel_C.bcg" |= with evaluator [ (not ("CRASH !3" or "GET !3 !2"))* ] ( [ "GET !1 !2" ] INEVITABLE ('CRASH ![31]' or "GET !3 !2") and [ "GET !2 !2" ] INEVITABLE ('CRASH ![32]' or "GET !3 !2") ); expected TRUE; -- dataless formula #7 for message 3 and receiver 1 "rel_rel_C.bcg" |= with evaluator [ (not ("CRASH !1" or "GET !1 !3"))* ] ( [ "GET !2 !3" ] INEVITABLE ('CRASH ![12]' or "GET !1 !3") and [ "GET !3 !3" ] INEVITABLE ('CRASH ![13]' or "GET !1 !3") ); expected TRUE; -- dataless formula #8 for message 3 and receiver 2 "rel_rel_C.bcg" |= with evaluator [ (not ("CRASH !2" or "GET !2 !3"))* ] ( [ "GET !1 !3" ] INEVITABLE ('CRASH ![21]' or "GET !2 !3") and [ "GET !3 !3" ] INEVITABLE ('CRASH ![23]' or "GET !2 !3") ); expected TRUE; -- dataless formula #9 for message 3 and receiver 3 "rel_rel_C.bcg" |= with evaluator [ (not ("CRASH !3" or "GET !3 !3"))* ] ( [ "GET !1 !3" ] INEVITABLE ('CRASH ![31]' or "GET !3 !3") and [ "GET !2 !3" ] INEVITABLE ('CRASH ![32]' or "GET !3 !3") ); expected TRUE; -- value-passing formula (a single formula is needed) "rel_rel_C.bcg" |= with evaluator forall i, m:nat among { 1 ... 3 } . [ (not ({ CRASH !i } or { GET !i !m }))* . { GET ?j:nat !m where j <> i } ] INEVITABLE ({ CRASH ?k:nat where (k = i) or (k = j) } or { GET !i !m }); expected TRUE end property ------------------------------------------------------------------------------- -- PART 4: COMPARISON OF LNT AND LOTOS SPECIFICATIONS ------------------------------------------------------------------------------- -- executing the former demo in LOTOS % (cd LOTOS ; echo "" ; svl) -- comparison of the LTSs generated from LOTOS and LNT "fifo.bcg" = generation of "fifo.lnt"; "interface.bcg" = generation of "interface.lnt":INTERFACE; strong comparison "fifo.bcg" == "LOTOS/fifo.bcg"; strong comparison "interface.bcg" == "LOTOS/interface.bcg"; strong comparison "crash_trans.bcg" == "LOTOS/crash_trans.bcg"; strong comparison "rel_rel_A.bcg" == "LOTOS/rel_rel_A.bcg"; strong comparison "rel_rel_B.bcg" == "LOTOS/rel_rel_B.bcg"; strong comparison "rel_rel_B_compo.bcg" == "LOTOS/rel_rel_B_compo.bcg"; strong comparison "rel_rel_C.bcg" == "LOTOS/rel_rel_C.bcg"; -- cleanup % SVL_COMMAND_FOR_CLEAN "(cd LOTOS ; svl -clean)" -------------------------------------------------------------------------------