Modeling and Consistency Checking Based on Category for Web Navigation Behavior

Using formal method is an effective methodology for modeling and verifying software system. Category theory provides a kind of common language, tool, thinking method and study means for other mathematics subjects, in which a sketch as a formal structure is a specification based on graphs. This paper gives a linear sketch for the Web navigation behavior, and constructs a formal model based on the category theory, which satisfies the given requirements and the specification described by the sketch, and proposes a method of the model consistency checking by constructing the free category, and discusses the security of the navigation model. Some rules of the link-security and return-security together with the corresponding approach to security checking are given as well as.