The Library
Investigating post-completion errors with the alloy analyzer
Tools
Tools
Tools
Boyatt, Russell and Sinclair, Jane (2007) Investigating post-completion errors with the alloy analyzer. University of Warwick. Department of Computer Science. (Unpublished)
|
PDF
WRAP_Boyatt_cs-rr-433.pdf - Published Version - Requires a PDF viewer. Download (612Kb) | Preview |
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: |
|
||||
| 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) | ||||
| Date of first compliant deposit: | 28 July 2016 | ||||
| Date of first compliant Open Access: | 28 July 2016 | ||||
| Related URLs: |
Request changes or add full text files to a record
Repository staff actions (login required)
 |
View Item |
Downloads
Downloads per month over past year
