Uppaal is free to download and very easy to install and use. The exercise can be done by high school or undergraduate students without any prior knowledge, after a short explanation of what a state diagram is, and a demo that walks through the basic features of Uppaal. (The explanation should cover Uppaal's notation ? and ! for input and output actions on channels, the notion of deadlock, explain how you edit the state diagrams, and show the simulator and the verifier, including how the verifier will produce counter-examples that you can step through in the simulator.)
A model checker does not work with the real system, but a model of the system - hence the name. Uppaal uses state diagrams as models. Apart from a diagram describing the system we want to analyse, we also need to describe some desired properties. These properties are called queries.
Install Uppaal and then download & save the files below:
The file atm.xml provides a model of an ATM (Automated Teller Machine, or cashpoint), a customer, and a bank. To keep things simple, the bank only has one ATM and one customer. There customer, called Eric carries Eric.cash_in_pocket euro in his Wallet. The ATM has with ATM.in_till euro in till. The Bank is the back-end system of the bank, and keeps track of Eric's balance in Bank.balance.
Eric interacts with the ATM to withdraw cash from the machine. The ATM in turn communicates with the Bank, to make sure that the bank correctly keeps track of the balance of Eric's bank account.
Intially, Eric has no cash in his pocket. You can check this in Uppaal by clicking on the system left of Eric, and then on clicking on Declarations. Eric has a balance of 80 euro in his bank account, and the ATM has 200 euro in the till.
The file atm.q expresses two properties of the systems: namely that Eric always owns 80 euro (since the model does not include the possibility for him to spend any money) and that the system should not deadlock.
Uppaal tip: under the menu Options:Diagnostic Trace select the option Shortest to let the verifier generates a counterexample in the simulator.
There is still something in the model of the ATM that is not realistic: with this lower amount of money in the till something can happen in the model which would be impossible in reality. Try to figure out what this is. You can do that by simulating the model for a while, or by letting Uppaal do a random simulation. (Hint: Eric wants to do some shopping and needs a lot of cash.)
Change the model of the ATM to improve this.
Once you have done this, add a query to the verifier to check that the problem has been avoided. The query should express the obvious reality check for the ATM. Of course, the adapted model still should not deadlock!
A Eric.cash_in_pocket + Bank.balance == 80or the slightly weaker property
A Eric.cash_in_pocket + Bank.balance <= 80
Imagine what the consequences would be if ATM or the back-end in the bank would crash at some point, say due to a power failure, at a moment in time when the properties above do not hold. Can you understand why the bank would want that at least one of these two properties to always hold?
Try to improve the system so that one of the properties above is always guaranteed. Of course, you can use Uppaal's verifier to check this. You should make sure that the changes you make are realistic: this is not something that Uppaal can check for you!
Suppose the ATM can crash just before it wants to pay out some money. After the crash the ATM will re-boot, returning to the initial state READY. We can model this in the ATM by adding an arrow from the state READY_TO_PAY_OUT to the state READY.
Add the arrow above, and then improve the model of the ATM further so that the ATM recovers from this crash in a correct way: the ATM should return the banking card to Eric; you can choose for yourself whether the ATM still pays out the cash that is due to Eric, or whether it contacts the bank to cancel the debit of Eric's account. (Hint: you can add an extra variable to the declarations of the ATM so that after a re-boot the ATM can see that it has crashed.)