Investigating post-completion errors with the alloy analyzer

[thumbnail of WRAP_Boyatt_cs-rr-433.pdf]
Preview
PDF
WRAP_Boyatt_cs-rr-433.pdf - Published Version - Requires a PDF viewer.

Download (627kB) | Preview

Request Changes to record.

Abstract

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 interactive 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.

Item Type: Report
Subjects: Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software
Divisions: Faculty of Science, Engineering and Medicine > Science > Computer Science
Library of Congress Subject Headings (LCSH): Computer software -- Development, Operating systems (Computers), Parallel processing (Electronic computers), Sequential processing (Computer science)
Publisher: University of Warwick. Department of Computer Science
Official Date: 2007
Dates:
Date
Event
2007
Completion
DOI: CS-RR-433
Institution: University of Warwick
Theses Department: Department of Computer Science
Status: Not Peer Reviewed
Publication Status: Unpublished
Access rights to Published version: Open Access (Creative Commons open licence)
Date of first compliant deposit: 28 July 2016
Date of first compliant Open Access: 28 July 2016
Related URLs:
URI: https://wrap.warwick.ac.uk/61599/

Export / Share Citation


Request changes or add full text files to a record

Repository staff actions (login required)

View Item View Item