Abstract: A formal model representing the navigation behavior of a Web application as a Kripke structure is proposed, and an approach that applies the model checking technique to verify Web application design is presented. A collection of properties that a Web application should satisfy is specified in CTL formulas, and then model checked against the formal model by using model checker NuSMV. A prototype that embeds the NuSMV verifier automatically parses the XMI output of UML tool and builds the NuSMV program.

Key words: CTL, model checking, verification, Web application