【作者】 陈圣波；

【导师】 缪淮扣；

【作者基本信息】 上海大学 ， 计算机应用技术， 2008， 博士

【摘要】 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模型的转换。更多还原

【Abstract】 Web application is an interactive one with a multi-tier architecture which is complicated, distributed multi-composition and can run at multi-platform and can implemented by multilingual programs. It provides an entirely new way to deploy software applications to end users. Web applications are usually composed of front-end user interfaces in Web browser, back-end servers including web server, application server and database server etc. With prevalence of Internet and rapid development of some technology such as distributed computing, component-based developing and Web services, Web applications have been integrated into many business critical systems and public transaction processing systems. The analysis and modeling of Web applications are very difficult due to its complexity, dynamicity, heterogeneity and the diversity of its links and compositions. How to ensure the reliability and quality of Web applications introduces new challenges to software engineering community.Testing is a most fundamental approach to improving the reliability and the quality-assurance of software. And model-based testing provides effective ways to implement the testing of Web applications and realizes the automation of test procedure completely. Therefore, it is of the utmost importance to construct appropriate models for model-based Web application testing. This is research emphases in this paper.Modeling of the system lays a foundation and source of the generating test case and testing execution. Whether the models constructed are consistent with users’ requirement or not can be verified by model checking. Model checking is an automatic, model-based, property-verification approach and wildly used in automatic verification of finite state systems. It analyzes the entire state space of the model in order to determine whether the model violates the properties or not. Model checker produces counterexamples that can be used to diagnose the faults in the system as soon as a violation of the property is detected.This paper focuses on modeling and verifying Web applications available to facilitate to generating test cases. The research work includes: 1. approaches to modeling Web applications by FSM including the Web application portioning and the interactions and compositions of FSM; 2. the formal navigation models of Web applications and the verifications of their consistency and security of navigation; 3. the modeling and verifying Web browser interactions. At last, transforming UML Models to FSM Models has been done. The details are as follows:The most important thing of concerns for model-based testing is to model the Web application. This paper proposes a three-dimensional modeling approach based on FSMs and the concept of Logic Component (LC). We employ a component-interaction automata modeling language (CIAML) to model the interactions between Web pages and back-end servers, software modules and components etc. An approach to modeling the Web page is presented. The model of the whole Web application is modeled by the composition of LCs.From users’ view, the navigation behavior in the client-side is a specific feature introduced by Web applications. This paper studies the modeling and verification of Web navigation. Consequently, the key issues lie in formal modeling and properties generation of Web navigation. Kripke structure is one presentation of FSM. An approach to illustrating the navigation using Kripke structure in Web applications is presented, namely, the navigation models are described formally by Kripke structure exploited. The properties to be verified are generated from threefold: design models of Web application, security strategy of Web navigation and users’ experience models (UXM). Consistency criterion of Web navigation corresponding to design models and the method to generate verifying properties are laid out. Besides, according to users’ experience models, we take Web browser interactions into account and give out verifying properties from UXM. UXM are further used to improve on and modify the design models and navigation models.Web applications can only be accessed through dedicated client systems called Web browsers. The users can press the Back or Forward buttons to negatively influence the behaviors of Web application navigation. Existing navigation models are static ones on the whole. Users’ navigation paths are all determined on stage of model design. Web browser interactions that have not been taken into account make them difference from practical navigation in Web applications. Accordingly, special care is taken on Web browser interactions during the user’s traversal within hypermedia space in order to specify possible inconsistencies between Web browser interfaces and user cognitions. We give out the concept of Safety Critical Region (SCR) and propose an approach to modeling on-the-fly navigation models.The Kripke structure is employed to describe the on-the-fly navigation models. Coverage criteria of Web browser interactions, such as, node coverage, transition coverage triggered by actions, SCR coverage, are exploited to derive the properties of Web Browser interactions in CTL. Ultimately, we use SMV, the model checking tool, to verify the on-the-fly navigation models.Finally, an approach to transforming UML models to FSM models is proposed. Corresponding transformational rules are presented. We mainly focus on the transformation of UML statecharts to FSM models. First of all, XMI and SCXML are used to describe as texts of UML models and FSM models, respectively. And second, take advantage of the transformation rules, it can automatically implement the transformation between two texts. In this paper we design a model transformer to transform UML models to FSM models.更多还原