Using a verification system to reason about post-completion errors
Paul Curzon, ANN E. BLANDFORD · 2000
Faults in the way a system works are often attributed to user error. Formal verification is one approach advocated to help avoid errors. Previous work has concentrated on ensuring that implementations meet specifications or that safety or liveness properties hold of a specification. However, systems verified in this way are still prone to catastrophic user errors. The designs of computer systems can often provoke certain classes of user errors. Indeed such problems are ubiquitous in every-day life. An example is the post-completion error where the user omits some necessary termination action. Work from the fields of cognitive psychology and human computer interaction suggest that such user errors are avoidable if systems are designed appropriately. We demonstrate that, by adopting a user-centric approach to system verification, formal proof methods can both detect and prove the absence of such system design errors. Furthermore, this approach can be integrated with traditional system verification methods. In particular, we show how the HOL proof system can be used to verify the absence of post-completion errors within the framework of a traditional hardware verification.