document: Model checking cobweb protocols for verification of HTML frames behavior 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 .
doc_bio_tags: B I O O O O O B B O B O O O B O O O O O O O O O O O O O O O O O O O B O O O O O O O O O O O O O O O O O O O O O O O O O B I O O O O O O O O O O B I O O O B O O O O O O O O B B O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O B O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O O