To model NetBill, we view each agent as a finite state machine, and use CSP processes to encode them. A CSP process denotes a set of sequences of events, where an event represents a state transition of the state machine; states are implicit.
Figures 2, 3, and 4 present
simplified versions of the consumer, the merchant, and the bank
processes respectively.
Note that -> is a form of sequential composition, || and
[]
are choice operators (with ||, the choice is completely arbitrary,
whereas [] gives preference to unblocked processes),
STOP denotes process termination,
! and ? are the
communication primitives (for example, coutm!goodsReq sends the
message goodsReq on the channel coutm, and
cinm?x receives a message from channel cinm, and binds the
variable x to
the message).
CSP uses a synchronous model of communication between processes. Since
we are modeling a distributed system, we need to simulate asynchronous
communication. For communication from agent a to agent b, we use
two channels aoutb and bina, and a process that reads
anything from the first channel and writes it to the second. This
process can be easily modified to introduce communication failures as needed.
Processes ABORT, SUCCESS, ERROR, NO_FUNDS,
NO_TRANSACTION, END and FAIL are mapped to the CSP
STOP process. We use them to improve readability of the code.
Figure 2: The consumer process.
Figure 3: The merchant process.
Figure 4: The bank process.
