Russell Boyatt and Jane Sinclair Investigating post-completion errors with the Alloy Analyzer
Post-completion errors are a particular kind of error found in interactive systems. This type of error occurs through the incorrect sequencing of goals and sub-goals, when the primary goal is achieved before all of the prequisite sub-goals have been satisfied. This paper shows how we can check for this property in a formal model of an interactive system. Specifically, we suggest that lightweight formal methods, such as the Alloy structural modelling language, are particulary well suited for this task. As a case study we develop two example interactiv e systems. The first is the ubiquitous chocolate machine, where both the chocolate and change must be delivered to the customer. The second model is of a typical cash machine and explores the problems of returning the cash and the cash card in the correct order. Both of these models are developed in the Alloy language.