A Tabular Interface for Automated Verification of Event-Based Dialogs
Abstract
In this report, we investigate the feasibility of a tabular interface for the specification and analysis of event-based dialogues. These dialogues are used to define high-level descriptions of interactive systems, and they are based on Olsen's Propositional Production System (PPS) notation. The simulation of the abstract user-system dialogue is an effective means of matching a design with an expected task model. Monk and Curry have produced a prototype dialogue simulation tool, the Action Simulator, which demonstrates how a tabular paradigm can be used to specify and simulate the dialogue. Further analysis of the dialogue can uncover problems which are not, so easy to detect with simulation. If we view the dialogue as defining a finite state machine, then we can make use of powerful model verification tools, such as Clarke's Symbolic Model Verifier (SMV) tool, to perform more powerful analyses on the dialogue. We also find that the tabular paradigm for input is an interesting alternative to the input language for the SMV tool. We provide in this report a mechanical translation from the tabular dialogue specification into SMV and provide templates or heuristics for various reachability analyses using the Computation Tree Logic (CTL) formalism. This research, therefore, presents the beginnings of two significant contributions. For the HCI community, we show how model verification tools can be used to provide a more powerful analytic technique beyond simulation for the specification and design of interactive dialogues. For the model verification community, we demonstrate the possibility of developing a simpler interface to specify and analyze certain finite state machines.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jul 28, 1994
- Accession Number
- ADA286065
Entities
People
- Gregory Abowd
- Hung-ming Wang
Organizations
- Carnegie Mellon University