Abstract:
This article describes a framework to formally model and analyse human behaviour. This is shown by a
simple case study of a chocolate vending machine, which represents many aspects of human behaviour. The case
study is modelled and analysed using the Maude rewrite system. This work extends a previous work by Basuki
which attempts to model interactions between human and machine and analyse the possibility of errors occurring
the interactions. By redesigning the interface, it can be shown that certain kinds of error can be avoided for some
users. This article overcomes the limitation of Basuki's approach by incorporating many aspects of user behaviour
into a single user model, and introduces a more natural approach to model human-computer interaction.
