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.