Money and Goods Atomicity for NetBill

Recall the money conservation property given by the sum in Formula 1 at the start of this section. Since we do not have electronic coins, and we have only have one run of the protocol, this property is satisfied exactly when a debit is matched by a credit, or vice-versa. In CSP, this can be specified as:

SPEC1 = STOP ||
	((debitC -> creditM -> STOP) []
	 (creditM -> debitC -> STOP))

Note that the third component of the specification, creditM -> debitC -> STOP, could be omitted, since in our specification of NetBill a debitC always happens before creditM, if they ever happen. To check this specification using FDR, we first combine the consumer, merchant and the bank processes with an appropriate communication process, and then hide all of the irrelevant events (the Appendix gives the details of the communication process, process combination and event hiding); call the resulting system SYSTEM1. Finally, we check that SYSTEM1 is a refinement of SPEC1 with the FDR command line:

Check1 "SPEC1" "SYSTEM1"

Check1 is a two argument command that determines whether its second argument is a failure/divergence refinement of its first.

Goods atomicity for NetBill is more complex and involves reasoning about the messages' send and receive synchronization events: cinm.encryptedGoods (this indicates C's receipt of the message with the encyptedGoods), cinm.paymentSlip (this indicates C's receipt of the paymentSlip message), and cinb.paymentSlip (this indicates M's receipt of the paymentSlip message). Now, in order for C to ``receive'' the goods, C must receive both the encryptedGoods message and the encryption key (included in the paymentSlip message). We can now specify goods atomicity as follows:

SPEC2 =
   STOP ||
   (cinm.encryptedGoods -> 
      (STOP || 
       (debitC ->
          creditM ->
            ((cinb.paymentSlip -> STOP) ||
             (cinm.paymentSlip -> STOP)))))

For simplicity, this specification is somewhat less general than our previous definition of goods atomicity (in particular, the above specification says that goods must be paid for before they are received, whereas the previous definition stated that goods are received if and only if they are paid for and that the order of receipt and payment does not matter).

Our NetBill model satisfies both SPEC1 and SPEC2; the full FDR code and excerpts from the model checking session appear in the Appendix.