Hyperdocuments as automata: verification of trace-based browsing properties by model checking
Hyperdocuments as automata: verification of trace-based browsing properties by model checking
复制标题
作为自动机的超文档：通过模型检查验证基于跟踪的浏览属性
DOI：
10.1145/267954.267955
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
Cyrano Ruiz Cabarrus
中科院分区：
文献类型：
--
作者：
P. D. Stotts;Richard Furuta;Cyrano Ruiz Cabarrus
我们提出了一种超文档视图，其中每个文档在其链接中编码其自己的浏览语义。这就需要在抽象地看待超文档的方式上进行思想上的转变。不是将文档的链接视为定义静态有向图，而是将它们视为定义抽象程序，称为文档的链接自动机。引入了一种称为html *的分支时态逻辑符号，用于指定文档在浏览期间应该显示的属性。一种称为模型检查的自动程序验证技术用于验证html *子集中的浏览规范是否符合链接自动化中定义的行为。我们首先将这些技术应用于几个Trellis文档，然后应用于一个Hyperties文档，以此来说明这些技术的通用性。
We present a view of hyperdocuments in which each document encodes its own browsing semantics in its links. This requires a mental shift in how a hyperdocument is thought of 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 used to verify that browsing specifications in a subset of HTL* are met by the behavior defined in the links-automation. We illustrate the generality of these techniques by applying them first to several Trellis documents and then to a Hyperties document.