In this assessment, your team will use the Prism model checker to design and implement a

model for a vending machine controller: software for managing selection, payment and

delivery of drink products to the customer.

The vending machine stores amounts of three different kinds of drinks: Kiwi$-$Cola, Bolt

Energy Drink and Clear Water. A customer uses the Drink Selection Interface component to

select a drink kind. Once a selection is made, the customer uses EFPOS to pay via the

Payment component. The Drink Dispenser component ensures the drink is delivered to the

customer and the total amount of that kind of drink is decreased. Once the transaction is

completed, the vending machine is ready for the next customer. If an error interrupts the

transaction at any time, the vending machine is permanently placed in maintenance mode

such that no further transactions are allowed.

System Components Details

The system comprises the following components to be modelled

Drink Selection Interface Component

Initially, there is no drink kind selected. Once a selection is made then payment is due. The

customer may change their selection before payment is completed. A customer should never

pay for a drink if there are none available of that kind. If no drinks of any kind are available

then the vending machine is permanently placed in maintenance mode.

EFPOS Payment Component

The payment component allows the customer to use their EFPOS card to pay for their

selection, using a keypad to enter their PIN for verification. If the PIN is incorrect then the

transaction is cancelled and the vending machine is reset to begin a new transaction.

Drink Dispenser

Initially, there are at least three of each drink kind available. Once payment is made, the drink

dispenser delivers the drink. The amount of the drink is decreased. When the amount of

drinks has reached zero it cannot be further decreased.

Scenarios

Use Prism to simulate your model on the following user stories

$1.$ Customer selects Clear Water and pays via EFPOS, with correct pin

$2.$ Customer selects Kiwi$-$Cola and pays via EFPOS, with incorrect pin

$3.$ Customer selects a drink but an error occurs

$4.$ Customer selects a Clear Water but there are no drinks of this kind available

$5.$ Customer purchases Bolt Energy Drink and then purchases Clear Water.

Temporal Logic Formula Verification

Specify Temporal logic Formulae to determine the validity of the following properties

$1.$ Once in$,$ the vending machine never leaves maintenance mode

$2.$ If an error occurs then maintenance mode occurs in the next state

$3.$ A customer cannot not pay for an unavailable drink

$4.$ When a customer pays for a drink it is dispensed