Hyperdocuments as automata: trace-based browsing property verification
Conference Paper
Overview
Identity
Additional Document Info
Other
View All
Overview
abstract
1922 ACM. In many hypertext systems, meaningfully traversing a document depends on capabilities, features, and navigational AIDS that are part of the browser implementation. For example, if a reader browses to a node that has no out links, then backing up, or "warping" to the table of contents can allow the browsing session to continue. If hyperdocuments are to become interchangeable among hypertext systems, rather than being readable only on the systems from which they are authored, one obvious but complex approach is to try and standardize on (most likely, very many) browsing features and behaviors, forming some standard union of the capabilities of current major implementations. This approach molds (or perhaps restricts) future systems, since new browsing "features" must then be worked into such a standard. An alternate approach, used in this paper, is to de-emphasized browser features and emphasize inherent document structure with browsing semantics. An author should be able to create document structure so that the desired meaningful access patterns are inherently allowed by links rather than by browser capabilities. We present a method of analyzing the browsing properties of a hypertext document by examining the links alone. This method is not specific to any particular hypertext system or document authoring format. With it, an author can be certain that a document will allow particular access patterns when read on any browser implementation that has a single navigation operation: direct link following. The method requires a mental shift in how a hyperdocument is conceived abstractly. Instead of treating the links of a document as defining a static directed graph, they are thought of as defining an abstract program, termed the links-Automaton of the document. A branching temporal logic notation, termed HTL, is introduced for specifying properties a document should exhibit during browsing. An automated program verification technique called model checking is then used to verify that these specifications are met by the behavior of the links-Automaton. We illustrate the generality of our technique by applying it first to a Trellis document, and then to a Hyperties document.
