软件测试是保证软件质量的一种重要手段，而复杂的Web应用对测试提出了新的要求.提出一种Web应用测试生成与约简方法，该方法对Web应用导航进行形式建模，使用模型检验导航安全性质所输出的反例分化模型，然后根据分化模型产生测试序列，依据Web应用的特性对测试序列集进行约简.实例演示表明该方法的有效性.

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.