Issue
Article
Vol.28 No.2, April 1996
Article
Issue
Issue |
Article |
Vol.28 No.2, April 1996 |
Article |
Issue |
The work outlined in this position paper represents a good example of synergy between HCI and Software Engineering research. One year ago, the first author became aware of the work that Andrew Monk and Martin Curry from the University of York had been doing on a dialogue specification tool called the Action Simulator, an Excel spreadsheet template and macro set for describing and simulating dialogue descriptions [1]. The main advantages of that work were the accessibility of the tool and its ability to simulate dialogue descriptions. The former means that just about everyone will be able to use the tool, while the latter means that it is possible to validate a formal dialogue description against a set of real-world scenarios. The simulation of the abstract user-system dialogue is an effective means of matching a design with an expected task model. But simulation is not a feasible approach to proving other properties of the dialogue, for example, certain global reachability features that require an exhaustive search through a potentially large set of possible execution paths. Analysis of this kind of dynamic or temporal dialogue property is not practical through exhaustive simulation.
The ideas behind the Action Simulator are intriguing and we have since pursued a connection with an emerging software engineering research technology -- model checking -- to address some of the shortcomings of dialogue simulation. The Action Simulator uses a tabular representation of Olsen's Propositional Production System (PPS) [4]. The PPS representation of dialogue is formally equivalent to a finite state machine representation. In recent years, there have been major advances in software engineering research in the area of model checking -- a technology for efficient, automated verification of finite state machines. In particular, a tool developed at Carnegie Mellon under the direction of Ed Clarke, called the Symbolic Model Verifier (SMV), provides particularly efficient exhaustive search on very large state machines [3]. The problem with these model checkers -- and this is an important consideration for interactive system design -- is that they are not the easiest tools to use. Nor have they been used widely for verification tasks outside of the hardware domain.
A marriage of ideas from the Action Simulator and state-of-the-art model checking presents a win-win situation for HCI and Software Engineering research. The two technologies came from somewhat separate research disciplines, yet the combination of the two makes the whole stronger than the parts. We have shown that translating the tabular representation of the Action Simulator dialogue into the state machine language of SMV allows for automatic verification of a number of dynamic temporal dialogue properties [5]. Olsen, Monk and Curry have suggested a number of interesting dialogue properties that can be expressed using the PPS model [5], but they do not provide a way to efficiently prove that a given dialogue description meets any of those properties. Translation into SMV makes that automatic verification possible and practical. Furthermore, a production rule interface to SMV -- particularly the tabular version demonstrated in Action Simulator for the pre- and post-condition semantics -- is an attractive alternative to the current textual language.
Figure 1 shows the overall dialogue development method that combines the dialogue formulation and validation (steps 1 and 2) of Action Simulator with the verification (step 4) made possible by SMV. In [5], Wang and Abowd showed that a mechanical translation (step 3) from Action Simulator to SMV was possible. That paper also demonstrates how most of the dialogue reachability properties suggested by Olsen, Monk and Curry could be expressed as Computation Tree Logic (CTL) expressions. SMV can verify whether a state machine representation satisfies an arbitrary CTL expression. The details of this translation and the formulation of CTL dialogue properties is available in [5].
Figure 1: The Dialogue Development Method
For certain CTL expressions -- ones that rely on universally quantified phenomena (indicated by the "A" path quantifier in CTL)-- when SMV reports that a property is not satisfied by the state machine, it produces a counter-example in the form of an execution path. It would be very instructive to a designer to see this counter example visualized in the simulation environment so that the reason for the property violation might be more easily observed.
The authors have created an initial prototype of a complete dialogue analysis tool which combines the tabular interface of the Action Simulator with the model checking capabilities of SMV. This tool has been implemented using the tcl/TK toolkit for a unix workstation, which means we have had to sacrifice the wide availability of the tool (Excel) that was a feature of the Action Simulator. In return, we now have the full power of a state-of-the-art model checker for verifying and visualizing a large class of dynamic reachability properties of the dialogue.
Whereas this synergy between HCI and Software Engineering research is pleasing, there are some problems with this approach. There is an underlying assumption in the Action Simulator work that designers find it easy to formulate pre- and post-condition semantics of a production system. To the best of my knowledge, there is no empirical evidence to support this claim. My own anecdotal experience shows that students do not find it all that straightforward to go from a set of loosely expressed task scenarios to a development of a structured dialogue in the tabular form. The main problem is that they find it hard to grasp what dialogue state is all about. Apart from that formulation problem, I do see one advantage of the tabular representation. Assuming that you are comfortable with the list of events you want to model and the state of the dialogue, the tabular representation gives a good visual cue as to when the dialogue formulation process is complete -- you simply have to fill in all of the cells in the table. From an engineering perspective, that is an advantage.
Efficient techniques for dialogue verification address one of the difficulties in dialogue development -- computational state explosion. But there is another problem -- descriptive state explosion, or the difficulty in representing a dialogue description in a compact form for communication purposes -- and it does not appear that a tabular representation fares as well on this point. Large dialogue descriptions (many events or many dialogue state fields) will produce unwieldy tabular descriptions and unless there is some convenient way of collapsing the table while still communicating its meaning to the designer, this approach is likely to fail.
Another underlying assumption in this work is that dialogue properties are both important in the early stages of interactive system design and difficult enough to get right that designers will need the assistance of these kinds of techniques and tools. Again, I do not know of any evidence to establish that assumption. One type of property that seems very amenable to automated verification is the undo problem, but as is discussed in Chapter 8 of [1], real undo is not a dialogue property but an application property. There is no reason why application semantics cannot be brought explicitly into the state of Action Simulator/PPS productions, but that will only serve to exacerbate the descriptive state explosion problem.
In the meantime, the kinds of properties that are very suited to this approach are reachability properties, deadlock and connectivity properties. These properties can also be calculated as graph traversal problems, as Thimbleby has shown, but the advantage of the approach described in this paper is that we do not rely on an explicit representation of the dialogue state transition graph and so we can address much larger state machines. The latest versions of the SMV tool also allow the computation of quantitative characteristics of individual state transitions, opening up the possibility to verify more explicit temporal properties of a dialogue specification.
SMV is a state-based language; it does not treat events as first-class state transition labels. This means that events must be encoded as non-deterministically set state variables. This is a technicality, but the practical ramifications are that some dialogue properties cannot be adequately expressed as CTL expressions (see [6] for more details on this point). It is unclear at the moment whether there is a reasonable alternative to SMV that would circumvent this problem.
The work described here is based on a production rule formalism for dialogue description and analysis. In [1], we have described a much wider range of dialogue models which vary along a number of dimensions such as overall expressive power of the underlying model (e.g., regular expressions vs. BNF grammars), support for concurrency (e.g., state transition networks vs. statecharts) and overall ease of notation (graphical vs. textual). Together with Alan Dix, I am currently investigating the development of general dialogue analysis tools which will allow for automatic translation between various dialogue models, allowing a designer to take advantage of particular notations as and when they are appropriate.
Lein Ton
Department of Informatics
Delft University
Delft, The Netherlands
Issue |
Article |
Vol.28 No.2, April 1996 |
Article |
Issue |