Hyperdocuments as automata: verification of trace-based browsing properties by model checking

ABSTRACT

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.

REFERENCES

• 1: J. M. Atlee , J. Gannon, State-Based Model Checking of Event-Driven System Requirements, IEEE Transactions on Software Engineering, v.19 n.1, p.24-40, January 1993 [doi>10.1109/32.210305 ]
• 2: Howard Barringer , Ruurd Kuiper , Amir Pnueli, Now you may compose temporal logic specifications, Proceedings of the sixteenth annual ACM symposium on Theory of computing, p.51-63, December 1984 [doi>10.1145/800057.808665]
• 3: Catriel Beeri , Yoram Kornatzky, A logical query language for hypertext systems, Hypertext: concepts, systems and applications, Cambridge University Press, New York, NY, 1992
• 4: Mordechai Ben-Ari , Zohar Manna , Amir Pnueli, The temporal logic of branching time, Proceedings of the 8th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.164-176, January 26-28, 1981, Williamsburg, Virginia [doi>10.1145/567532.567551]
• 5: BURSH, J. R., CLARK, E. M., AND MCMILLAN, K.L. 1989. Symbolic model checking: 10 to the 20 states and beyond. Carnegie Mellon and Stanford Universities.
• 6: BURSTALL, R. M. 1974. Program proving as hand simulation with a little induction. Inf. Process. 74, 308-312.
• 7: Brad Campbell , Joseph,M. Goodman, HAM: a general purpose hypertext abstract machine, Communications of the ACM, v.31 n.7, p.856-861, July 1988 [doi>10.1145/48511.48515]
• 8: Michael Capps , Brian Ladd , David Stotts, Enhanced graph models in the Web: multi-client, multi-head, multi-tail browsing, Proceedings of the fifth international World Wide Web conference on Computer networks and ISDN systems, p.1105-1112, May 1996, Paris, France
• 9: S. Christodoulakis , M. Theodoridou , F. Ho , M. Papa , A. Pathria, Multimedia document presentation, information extraction, and document formation in MINOS: a model and a system, ACM Transactions on Information Systems (TOIS), v.4 n.4, p.345-383, Oct. 1986 [doi>10.1145/9760.9764]
• 10: CLARKE, E. M. AND GRUMBERG, O. 1987. Research on automatic verification of finite-state concurrent systems. Ann. Rev. Comput. Sci. 2, 269-290.
• 11: E. M. Clarke , E. A. Emerson , A. P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications, ACM Transactions on Programming Languages and Systems (TOPLAS), v.8 n.2, p.244-263, April 1986 [doi>10.1145/5397.5399]
• 12: E. Allen Emerson , Joseph Y. Halpern, "Sometimes" and "not never" revisited: on branching versus linear time (preliminary report), Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.127-140, January 24-26, 1983, Austin, Texas [doi>10.1145/567067.567081]
• 13: E. Allen Emerson , Chin-Laung Lei, Modalities for model checking (extended abstract): branching time strikes back, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318620]
• 14: E. Allen Emerson , Jai Srinivasan, Branching time temporal logic, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, p.123-172, May 30-June 03, 1988
• 15: Richard Furuta , P. David Stotts, Structured dynamic behavior in hypertext, University of Maryland at College Park, College Park, MD, 1991
• 16: Richard Furuta , P. David Stotts, Interpreted collaboration protocols and their use in groupware prototyping, Proceedings of the 1994 ACM conference on Computer supported cooperative work, p.121-131, October 22-26, 1994, Chapel Hill, North Carolina, United States [doi>10.1145/192844.192888]
• 17: Dov Gabbay , Amir Pnueli , Saharon Shelah , Jonathan Stavi, On the temporal analysis of fairness, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567462]
• 18: Antony Galton, Temporal logics and their applications, Academic Press Professional, Inc., San Diego, CA, 1987
• 19: Frank,G. Halasz, Reflections on NoteCards: seven issues for the next generation of hypermedia systems, Communications of the ACM, v.31 n.7, p.836-852, July 1988 [doi>10.1145/48511.48514]
• 20: KAHN, K. AND GORRY, G.A. 1977. Mechanizing temporal knowledge. Artif Intell. 9, 67-95.
• 21: R Kowalski , M Sergot, A logic-based calculus of events, New Generation Computing, v.4 n.1, p.67-95, 1986
• 22: Fred Kröger, Temporal logic of programs, Springer-Verlag New York, Inc., New York, NY, 1987
• 23: LADD, B., CAPPS, M., STOTTS, D., AND FURUTA, R. 1995. Multi-Head/Multi-Tail mosaic: Adding parallel automata semantics to the Web. In Proceedings of the 4th International World Wide Web Conference (Dec. 11-14, Boston, Mass.). World Wide Web Consortium, Cambridge, Mass., 433-440. Available at http://www.w3.org/pub/Conferences/WWW4/ Papers/118/.
• 24: Leslie Lamport, "Sometime" is sometimes "not never": on the temporal logic of programs, Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.174-185, January 28-30, 1980, Las Vegas, Nevada [doi>10.1145/567446.567463]
• 25: LEE, R. M., COELHO, H., AND COTTA, J. C. 1985. Temporal inferencing on administrative databases. Inf. Syst. 10, 197-206.
• 26: Orna Lichtenstein , Amir Pnueli, Checking that finite state concurrent programs satisfy their linear specification, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.97-107, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318622]
• 27: J. W. Lloyd, Foundations of logic programming; (2nd extended ed.), Springer-Verlag New York, Inc., New York, NY, 1987
• 28: Zohar Manna , Amir Pnueli, Temporal verification of reactive systems: safety, Springer-Verlag New York, Inc., New York, NY, 1995
• 29: MANNA, Z. AND PNUELI, A. 1981. Verification of concurrent programs: The temporal framework. In The Correctness Problem in Computer Science, R. S. Boyer and J. S. Moore, Eds. Academic Press, New York, 215-273.
• 30: Gary Marchionini , Ben Shneiderman, Finding Facts vs. Browsing Knowledge in Hypertext Systems, Computer, v.21 n.1, p.70-80, January 1988 [doi>10.1109/2.222119 ]
• 31: Benjamin Charles Moszkowski, Reasoning about digital circuits, 1983
• 32: MURATA, T. 1989. Petri nets: Properties, analysis and applications. Proc. IEEE 77, 4 (Apr.), 541-580.
• 33: James Lyle Peterson, Petri Net Theory and the Modeling of Systems, Prentice Hall PTR, Upper Saddle River, NJ, 1981
• 34: Shlomit S. Pinter , Pierre Wolper, A temporal logic for reasoning about partially ordered computations (Extended Abstract), Proceedings of the third annual ACM symposium on Principles of distributed computing, p.28-37, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806733]
• 35: PNUELI, A. 1977. The temporal logic of programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science. IEEE, New York, 46-67.2
• 36: Wolfgang Reisig, Petri nets: an introduction, Springer-Verlag New York, Inc., New York, NY, 1985
• 37: Ben Shneiderman, User interface design for the Hyperties electronic encyclopedia (panel session), Proceeding of the ACM conference on Hypertext, p.189-194, November 1987, Chapel Hill, North Carolina, United States [doi>10.1145/317426.317441]
• 38: SINACHOPOULOS, A. 1989. Logics for Petri-nets: Partial order logics, branching time logics and how to distinguish between them. Petri Net Newsl. 3, 8 (Aug.), 9-14.
• 39: P. David Scotts , Richard Furuta, Browsing parallel process networks, Journal of Parallel and Distributed Computing, v.9 n.2, p.224-235, June 1990 [doi>10.1016/0743-7315(90)90048-T]
• 40: P. David Stotts , Richard Furuta, Petri-net-based hypertext: document structure with browsing semantics, ACM Transactions on Information Systems (TOIS), v.7 n.1, p.3-29, Jan. 1989 [doi>10.1145/64789.64791]
• 41: STOTTS, P. D. AND FURUTA, R. 1990b. Temporal hyperprogramming. J. Visual Lang. Cornput. 1, 3, 237-253.
• 42: P. David Stotts , Richard Furuta , J. Cyrano Ruiz, Hyperdocuments as automata: trace-based browsing property verification, Proceedings of the ACM conference on Hypertext, p.272-281, November 30-December 04, 1992, Milan, Italy [doi>10.1145/168466.171515]
• 43: WOLPER, Z. 1981. Temporal logic can be more expressive. In Proceedings of the 22nd IEEE Symposium on Foundations of Computer Science. IEEE, New York, 340-348.
• 44: Polle T. Zellweger, Active paths through multimedia documents, Proceedings of the International Conference on Electronic Publishing on Document manipulation and typography, p.19-34, May 1988, Nice, France

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Petri nets

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

  H. Information Systems
  H.5 INFORMATION INTERFACES AND PRESENTATION (I.7)

  I. Computing Methodologies
  I.7 DOCUMENT AND TEXT PROCESSING
      I.7.2 Document Preparation
          Subjects: Hypertext/hypermedia

General Terms:
Verification

Keywords:
Petri nets, browsing semantics, hypermedia, hypertext, model checking, temporal logic