Model checking cobweb protocols for verification of HTML frames behavior

ABSTRACT

HTML documents composed of frames can be difficult to write correctly. We demonstrate a technique that can be used by authors manually creating HTML documents (or by document editors) to verify that complex frame construction exhibits the intended behavior when browsed. The method is based on model checking (an automated program verification technique), and on temporal logic specifications of expected frames behavior. We show how to model the HTML frames source as a CobWeb protocol, related to the Trellis model of hypermedia documents. We show how to convert the CobWeb protocol to input for a model checker, and discuss several ways for authors to create the necessary behavior specifications. Our solution allows Web documents to be built containing a large number of frames and content pages interacting in complex ways. We expect such Web structures to be more useful in "literary" hypermedia than for Web "sites" used as interfaces to organizational information or databases.

REFERENCES

• 1: 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]
• 2: P. David Stotts , Richard Furuta , Cyrano Ruiz Cabarrus, Hyperdocuments as automata: verification of trace-based browsing properties by model checking, ACM Transactions on Information Systems (TOIS), v.16 n.1, p.1-30, Jan. 1998 [doi>10.1145/267954.267955]
• 3: 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]
• 4: B. Ladd, M. Capps, D. Stotts, R. Furuta, "Multi-head/Multi-tail Mosaic: Adding Parallel Automata Semantics to the Web, " World Wide Web Journal, O'Reilly and Assoc. Inc., vol. 1 (Proc. of the 4th Int'l WWW Conference, Boston, December 11--14, 1995), pp. 433--440.
• 5: Michael Capps , Brian Ladd , David Stotts, Enhanced graph models in the Web: multi-client, multi-head, multi-tail browsing, Computer Networks and ISDN Systems, v.28 n.7-11, p.1105-1112, May 1996
• 6: D. Stotts, J. Prins, L. Nyland, T. Fan, "CobWeb: Tailorable, Analyzable Rules for Collaborative Web Use," Technical Report CS-98-307, Dept. of Computer Science, University of North Carolina, Chapel Hill, 1998. http://www.cs.unc.edu/~stotts/papers/cobweb.ps
• 7: J. Navon, "Specification and Semi-Automated Verification of Coordination Protocols for Collaborative Software Systems," Ph.D. Thesis, Dept. of Computer Science, Univ. of North Carolina at Chapel Hill, June 2001; advisor: D. Stotts.
• 8: "Storyspace: A Hypertext Tool for Writers and Readers", http://www.eastgate.com/Storyspace.html
• 9: K. Jensen, G. Rozenberg, "High-level Petri Nets", Springer-Verlag, Berlin, 1991.
• 10: 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]
• 11: A. Pnueli, "A temporal logic of concurrent programs," Theoretical Computer Science, pp. 45--60, 1981.
• 12: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 13: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 14: "On-the-fly, LTL Model Checking with SPIN",

INDEX TERMS

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

Additional Classification:
  I. Computing Methodologies
  I.7 DOCUMENT AND TEXT PROCESSING
      I.7.2 Document Preparation
          Subjects: Markup languages

General Terms:
Documentation, Languages, Verification

Keywords:
HTML, browsing semantics, formal semantics, frames, literary hypertext, model checking, temporal logic, verification