Web应用的出现与盛行已将软件产业悄然带入规模化、复杂化的时代，提高其检测方法的自动化程度是当务之急。因此，我们采用基于模型的测试方法，以Web应用模型作为测试用例的来源。另外，为了使该模型与用户需求保持一致，必须对其应满足的各种性质进行验证。由此可知，模型构建是重要问题。 UML是理想的需求与设计模型语言，而模型检验与测试自动化要求模型用统一的形式化语言描述。鉴于大多数模型检验工具以FSM模型作为输入，本文提出了一种将UML模型形式化为FSM模型的方法，使之满足检测过程的需要。由于状态图代表系统行为的最小单位，本文从它们的形式化着手。另外，顺序图也是描述系统行为的常用模型，本文亦对其进行了研究并给出相应的形式化方法，不但服务于检测过程，也可用于后续归约过程。 高复杂度的Web应用软件将导致大规模的FSM模型，并可能引发状态爆炸。为了解决这个问题，我们利用归约指示及本文提出的一系列相关算法，对前期模型形式化后获得的系统FSM模型进行归约优化，产生只描述用户所要求测试的功能的FSM模型。该方法主要可分为两步，首先生成形式化的归约指示，将顺序图模型转换为FSM模型，然后以该形式化的归约指示为指导，对系统FSM模型执行归约操作，达到优化的目的。 FSM是我们研究工作中系统行为的重要描述形式，它为各环节传递信息，但计算机处理能力的局限性迫使模型只能以文本为载体。为了直观地了解其结构，本文给出了一种层次FSM模型的可视化方法。它首先读取模型文本，并以层次化的数据结构进行存储，然后根据用户要求查看的复合结点的对应关系，对相应FSM模型进行可视化。 为了支持本文提出的上述一系列方法，我们开发了相应工具原型，它利用XMI文件作为UML图形式模型的对应文本，并使用自定义的XML文件记录FSM模型。通过本文给出的读取算法，该工具先对文本中的模型信息进行分析，并以某种数据结构存储，然后根据用户需求，结合论文中提出的方法对UML模型进行形式化并对FSM模型进行优化与可视化。