Web应用是一种非常复杂的、分布式的、运行在不同平台、采用不同语言编写、多成分和多层结构的交互式应用,为用户提供了一种全新的部署软件应用的方式。典型的Web应用由前端浏览器图形界面和后端的Web服务器、应用服务器以及数据库服务器构成。Internet的普及以及组件、中间件和Web Services等技术的迅速发展和应用使Web应用渗透到国计民生的各个领域。Web应用的复杂性、动态性、异构性、组成成分和链接的多样性等使得对Web应用的建模和分析都相当困难。如何保证Web应用的可靠性和质量,是软件工程界面临的一个挑战。软件测试是提高软件可靠性和保证软件质量的一种最基本的手段。基于模型的测试技术是实现Web应用测试的有效途径,可以实现测试过程的自动化。因此,对Web应用系统建立模型对基于模型的Web应用测试极其重要,是本文研究的重点。对系统建立模型是后续测试用例生成和测试执行的基础和目标来源。模型相对于用户需求的正确与否通常可以通过形式验证来检验。模型检测是一种自动化的、基于模型的性质验证方法,广泛应用于有限状态系统的验证。它通过有效地搜索有限状态模型的整个状态空间判定性质是否满足,在系统不满足性质时提供的反例可以用于诊断系统的错误。本论文主要研究如何建立和验证适合于产生测试用例的Web应用模型。研究内容包括:Web应用的FSM建模方法,包括Web应用的划分方法,FSM的交互以及组合方法;Web应用的导航行为的形式化建模以及导航行为的一致性和安全性验证;Web浏览器交互行为的建模和验证;并给出了Web应用的UML模型向FSM模型的转换。具体内容如下:基于模型的Web应用测试的首要问题是为Web应用建立模型。论文研究提出了Web应用的三维FSM建模方法,给出了逻辑组件的概念,通过采用组件交互自动机建模语言(Component-Interaction Automata Modelling Language,CIAML)对Web页面和后台的服务器、软件模块、后台组件等的交互进行建模。并给出了Web页面的FSM建模方法。通过LC的组合实现对整个Web应用的建模。导航行为是Web应用的重要方面之一。本文以FSM和SMV为形式工具研究Web应用导航的建模和验证。因此,关键问题在于导航行为的形式建模和导航性质的产生。Kripke结构是FSM表示方式之一,论文给出了用Kripke结构描述导航行为的方法。从Web应用的设计模型、导航的安全策略以及用户体验模型三个方面产生导航行为验证的性质。提出了导航行为相对于Web应用设计的一致性准则以及根据一致性准则产生性质的方法,给出了描述导航安全策略的性质公式。同时,通过考虑到Web应用部署后的浏览器的交互行为,给出了Web应用的用户体验模型,并由用户体验模型来进一步对设计模型和导航模型进行了修订,从而进一步完善对Web应用导航行为的验证,可以回归地完善导航模型进而完善Web应用设计模型。Web应用只能通过称之为Web浏览器的客户端系统来进行访问。用户可以通过点击浏览器的“Back”和“Forward”按钮来消极地影响Web应用的导航行为。已有的Web页面导航模型基本上都是静态模型,在模型设计时就已经确定好了用户的导航路径,大都没有考虑Web浏览器的交互特性,这和现实的Web应用导航有很大差异。浏览器的行为可能影响Web应用的正确性:Web应用本身提供了正确的功能,但是当把它部署到其支持环境中后,由于浏览器的存在,就有可能导致功能失常。因此,论文特别考虑到了由于浏览器的交互而可能导致的和Web应用设计不一致的方面。也考虑到了cookies使能性、页面可缓存性,给出了安全敏感区SCR的概念,提出了Web应用的on-the-fly导航建模方法。采用Kripke结构来对该导航模型进行形式化描述,给出了由浏览器交互覆盖准则产生验证性质的方法,这些性质由CTL公式进行形式化描述,最后通过模型检测工具SMV对该带浏览器交互的Web应用的导航模型进行了验证。最后论文给出了UML模型到FSM模型的转换方法,重点研究了UML的状态图到FSM的转换。首先,采用XMI来给出了UML的表示方式,以及采用定制的SCXML来给出了FSM的表示方式。本文设计一个模型转换器,实现了UML模型到FSM模型的转换。