In this example, there are two versions of the systems. The first version is very coarse and it does not satisfy the requirements stated in the slides. However, it gives us valuable information about the behaviour of the systems based on this design.
The final version meets the requirements. The ideas behind these versions are described later.
This example consists of following files:
You can obtain the files from bank.tar.gz package.
gmake system.lstsThen you may examine the result visually by executing
tvt.illux system.lsts stylefile.col. Executing the commands above has the same effect as the following use of TVT tools
tvt.extendedrules system.xrules | tvt.parallel - | tvt.lsts2ag - | tvt.detlsts - | tvt.ag2lsts - | tvt.SBreduction - | tvt.illux - stylefile.colSometimes you may also want to have intermediary files. You can (g)make following files:
In the presentation there were three requirements which the system should satisfy.
Recording a withdrawal means that the withdrawn money is taken from the account or, if the bank is not sure whether or not the money was given to the customer, some kind of sign is left to database that the withdrawal should be checked later. It is not generally possible to make sure that the money of the last withdrawal was given to the customer. The uncertainity can be caused, for example, by a bulldozer or earthquake, which cuts the cable and thus the connection between the ATM and the bank.
Initially ATM process waits for the user to insert a card (ATM:card in) and initiate a withdrawal (ATM:withdraw). After that ATM sends a query to the bank (ATM:send query) to check if money can be given to the customer (if there is enough money in customer's account). Now there are three possibilities:
Bank waits in its initial state a query to be received (BANK:rec query). After that it decides that either
After these choises the bank process is again in its initial state waiting for another query.
Channel is unreliable first-in-first-out buffer with capacity one. It can convey at most two different messages from a sender to a receiver. When a message is put in to the channel (CH:in1 or CH:in2) it either can be lost (CH:lose) or passed through (CH:out1 or CH:out2).
There are four processes put in parallel in the composition of the whole system. Process number one is ATM which synchronises with two channel processes, numbered two and three (see system.xrules). Process number two is a channel which carries query messages from ATM to bank. Process number three is another channel from which ATM receives both ``withdrawal is allowed'' and ``bank refused to withdraw'' messages.
The fourth process is the bank, which is accordingly synchronised to the channel processes. It receives queries from process two and sends acceptance information of withdrawal to process three.
It is stated in the requirements that the inserted card should always be eventually given back to the customer. This does not hold in the system, because ATM deadlocks after error.
The system would not meet the requirements even if the card was given out after the error and ATM was reset to its initial state. The reason is that the bank may commit withdrawal (take the money from customer's account) even if the money is not given to the customer. This is fixed in the final version.
The main difference between the final and the first version is that the withdrawal is not committed before ATM has desided to give the money. This is ensured so that when ATM receives the ``withdrawal is allowed'' message, it sends acknowledgement (ATM:send done).
On the other hand, bank waits for the acknowledgement (BANK:rec done) and commits the withdrawal only when it is received.
If the bank does not receive an acknowledgement before it receives a new query or timeout occurs, it records an unclear withdrawal. In reality this would be a very unlikely situation.
Channel processes, as well as ATM and bank, can also consume time (execute CH:timeout actions) in their initial states.
Timeout actions of all processes are synchronised in parallel composition. Executing timeout action means that a certain amount of time passes. The time is long enough for underlying protocol to consider connection lost and give up sending messages that may be requested to sent.
Return to TVT project homepage.