Abstract: Software testing is important for ensuring software quality. To test complicated Web applications, some new problems need to be considered. In this paper, we present an approach to the generation and reduction of tests for Web applications. The navigational behavior of a Web application is described in a formal model. The model is partitioned according to the counterexamples generated by model checking against the given safety properties for navigation. The test sequences are generated according to the partitioned model, and reduced based on the characteristics of Web applications. The presented example shows that the described approach is effective.

Key words: model checking, model partition, redundancy reduction, test sequence, Web application