Web应用建模和验证方法研究
|
摘要
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模型的转换。
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.
软件测试是提高软件可靠性和保证软件质量的一种最基本的手段。基于模型的测试技术是实现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模型的转换。
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.
引文
[1]Anncliesc Andrews,Jeff Offut and Roger Alexander;Testing Web Applications by Modeling with FSMs,Software Systems and Modeling,4(3),August 2005.
[2]Grady Booch,James Rumbaugh,Ivar Jacobson.Unified Modeling Language User Guide,2nd Edition).Addison-Wesley,2005.
[3]James Rumbaugh,Ivar Jacobson,Grady Booch.Unified Modeling Language Reference Manual(2nd Edition).Addison-Wesley,Jul 19,2004.
[4]Jim Conallen,Building Web Applications with UML,Second Edition,Addison Wesley,2002.
[5]Alfred V.Aho,Ravi Sethi,Jeffrey D.Ullman and Monica S.Lam.Compilers:Principles,Techniques,and Tools(second edition).Addison-Wesley,Inc.2006.
[6]张素琴,吕映芝,蒋维杜,戴桂兰.编译原理(第2版).清华大学出版社.2005.
[7]Holzmann G.J..The model checker SPIN.IEEE Transactions on Software Engineering,1997,23(5):279-295.
[8]Vardi,M.Y.2001.Branching vs.Linear Time:Final Showdown.In Proceedings of the 7th international Conference on Tools and Algorithms For the Construction and Analysis of Systems(April 02-06,2001).T.Margaria and W.Yi,Eds.Lecture Notes In Computer Science,vol.2031.Springer-Verlag,London,1-22.
[9]McMillan KL.The SMV System for SMV version 2.5.4.http://www.cs.cmu.edu/～modelcheck/smv/smvmanual.ps,October,2006.
[10]Huth M and Ryan M.Logic in Computer Science:Modelling and Reasoning about Systems.Cambridge University Press,2004,170-255.
[11]Pnueli A.The temporal semantics of concurrent programs.Theoretical Computer Science,1981,13:45-60.
[12]Clarke EM and Emerson E A,and Sistla AP.Automatic verification of finite-state concurrent systems using temporal logic specifications.ACM Transactions on Programming Languages and Systems,1986,8(2):244-263.
[13]Clarke EM and Emerson E A.Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic.In Logic of Programs:Workshop,Yorktown Heights,NY,LNCS131.Springer-Verlag,1981:52-71.
[14]Browne M C,Clarke EM,Dill D L,Mishra B.Automatic verification of asynchronous circuits using temporal logic.IEEE Transactions on Computers,1986,35(12):1035-1044.
[15]Queille,J.and Sifakis,J.1982.Specification and verification of concurrent systems in CESAR.In Proceedings of the 5th Colloquium on international Symposium on Programming (April 06-08,1982).M.Dezani-Ciancaglini and U.Montanari,Eds.Lecture Notes In Computer Science,vol.137.Springer-Verlag,London,337-351.
[16]Sistla AP and Clarke EM.Complexity of Propositional temporal logics.Jonrnal of the ACM,1985,32(3):733-749.
[17]Lichtenstein O,Pnueli A.Checking that finite state concurrent programs satisfy their linear specification.In:Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages,New York,1985,97-107.
[18]McMillan KL.The SMV System for SMV version 2.5.4.http://www.cs.cmu.edu/～modelcheck/smv/smvmanual.ps,October,2006.
[19]Huth M and Ryan M.Logic in Computer Science:Modelling and Reasoning about Systems.Cambridge University Press,2004,170-255.
[20]Burch JR,Clarke EM,MeMillan KL,Dill DL,Hwang LJ.Symbolic model checking:1020states and beyond.Information and Computation,1992,98(2):142-170.
[21]Bryant R E.Symbolic Boolean manipulation with ordered binary decision diagrams.ACM Computing Surveys,1992,24(3):293-318.
[22] Biere A, Cimatti A, Clarke EM, and Zhu Y. Symbolic model checking without BDDs. In TACAS '99: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, London, UK. 1999,193-207.
[23] Courcoubetis C, Vardi M, Wolper P, and Yannakakis M. Memory efficient algorithms for the verification of temporal properties. In: Proc, of the 2nd International Workshop on Computer Aided Verification(CAV90), 1990,233-242.
[24] Alur R, Brayton RK, Henzinger TA, Qadeer S, Rajamani SK. Partial-Order reduction in symbolic state space exploration. In: Proc.of the 9th Int'l Conf, on Computer Aided Verification. LNCS 1254, Grumberg, springer-Verlag, 1997. 340-351.
[25] Berezin, S., Campos, S. V, and Clarke, E. M. 1998. Compositional Reasoning in Model Checking. In Revised Lectures From the international Symposium on Compositionality: the Significant Difference (September 08-12, 1997). W. P. Roever, H. Langmaack, and A. Pnueli, Eds. Lecture Notes In Computer Science, vol. 1536. Springer-Verlag, London, 81-102.
[26] Henzinger TA, Qadeer S, Rajamani SK, Tasiran S. An assume-guarantee rule for checking simulation. ACM Trans, on Programming Languages and Systems, 2002,24(1):51-64.
[27] Dams D. Abstraction in software model checking: Principles and practice (tutorial overview and bibliography ). Model Checking Software. Vol LNCS2318, Springer-Verlag, 2002, 53-67.
[28] Park D. Concurrency and automata on infinite sequences. In: 5th GI-Conference on Theoretical Computer Science. Berlin:Springer, 1981,167-183.
[29] Ball T, Majumdar R, Millstein T, and Rajamani SK. Automatic predicate abstraction of C programs. ACM SIGPLAN Notices, 2001, 36(5): 203-213.
[30] Graf S, Saidi H. Construction of abstract state graphs with PVS.In: Orna Grumberg, ed. Proceedings of the 9th International Conference on Computer Aided Verification (CAV '97), LNCS 1254, Springer-Verlag,1997,72-83.
[31] Ball T, Rajamani SK. Automatically validating temporal safety properties of interfaces. In: Matthew B D, ed. Proc of the 8th International SPIN Workshop on Model Checking of Software, LNCS 2057, Heidelberg: Springer-Verlag, 2001. 103-122.
[32] Henzinger TA, Jhala R, Majumdar R, and Sutre G Lazy abstraction. In: Proc, of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL'02), ACM SIGPLAN Notices, ACM, 2002, 37(1): 58-70.
[33] Corbett JC, Dwyer MB, Hatcli J, PasSreanu CS, Robby, Laubach S, and Zheng H. Bandera: extracting finite-state models from Java source code. In: Proc, of the 22nd International Conference on Software Engineering (ICSE '00), IEEE Computer Society Press, 2000. 439-448.
[34] Clarke E M, Grumberg O, Long D E. Model checking and abstraction. ACM Transactions on Programming Languages and System, 1994,16 (5):1512-1542.
[35] Clarke E, Grumberg O, Jha S, Lu Y, and Veith H. Counterexample-guided abstraction refinement. In: Proc, of International Conference on Computer Aided Verification (CAV00), LNCS 1855, Heidelberg: Springer-Verlag, 2000. 154-169.
[36] Chaki S, Clarke E M, Groce A, Jha S, and Veith H. Modular verification of software components in C. IEEE Transactions on Software Engineering, 2004, 30(6): 388-402.
[37] Godefroid P. Software model checking: the Verisoft approach. Formal Method in System Design, Kluwer Academic Publishers, 2005, 26(2):77-101.
[38] Havelund K and Pressburger T. Model checking Java programs using Java PathFinder. Software Tools for Technology Transfer, 1998,2(4): 366-381.
[39] [~1] Hong HS, Lee I, Sokolsky O, and Cha SD. Automatic test generation from Statecharts using model checking. In: Proceedings of the 1st International Workshop on Formal Approaches to Testing of Software (FATES '01), Aalborg, Denmark, Aug. 2001,15-30.
[40] Ammann PE and Black PE. Test generation and recognition with formal methods. In Intl. Workshop on Automated Program Analysis, Testing and Verification, Limerick, Ireland, 2000, 64-67.
[41] Gargantini A and Heitmeyer C. Using model checking to generate tests from requirements specifications. In ESEC '99, LNCS 1687, Springer-Verlag, 1999:146-162.
[42]Rene de Vries,Jan Tretmans.On-the-fly conformance testing using SPIN.Software Tools for Technology Transfer,2000,2(4):382-393.
[43]Hong,H.S.,Lee,I.,Sokolsky,O.,and Ural,H.2002.A Temporal Logic Based Theory of Test Coverage and Generation.In Proceedings of the 8th international Conference on Tools and Algorithms For the Construction and Analysis of Systems(April 08-12,2002).J.Katoen and P.Stevens,Eds.Lecture Notes In Computer Science,vol.2280.Springer-Verlag,London,327-341.
[44]Hong HS,Cha S D,Lee I,et al.Data flow testing as model checking.In:Proceedings of 25th International Conference on Software Engineering.Washington:IEEE Computer Society,2003:232-242.
[45]Ammann,P.E.,Black,P.E.,and Majurski,W.1998.Using Model Checking to Generate Tests from Specifications.In Proceedings of the Second IEEE international Conference on Formal Engineering Methods(December 09-11,1998).ICFEM.IEEE Computer Society,Washington,DC,46-54.
[46]Rajah,S.,Shankar,N.,and Srivas,M.K.1995.An Integration of Model Checking with Automated Proof Checking.In Proceedings of the 7th international Conference on Computer Aided Verification(July 03-05,1995).P.Wolper,Ed.Lecture Notes In Computer Science,vol.939.Springer-Verlag,London,84-97.
[47]Manna Z,Sipma H.Deductive Verification of Hybrid Systems Using SteP.HSCC 1998,305-318.
[48]R.V.Binder.Testing Object-Oriented Systems:Models,Patterns,and Tools.Addison-Wesley,2000.
[49]Chow,T.S.1978.Testing Software Design Modeled by Finite-State Machines.IEEE Trans.Softw.Eng.4,3(May.1978),178-187.
[50]T.Chow.Testing software designs modeled by finite-state machines.IEEE Transactions on Software Engineering,SE-4(3):178-187,May 1978.
[51]S.Fujiwara,G.Bochmann,F.Khendek,M.Amalou,and A.Ghedasmi.Test selection based on finite state models.IEEE Transactions on Software Engineering,17(6):591-603,June 1991.
[52]J.Offutt,S.Liu,A.Abdurazik,and P.Ammann.Generating test data from state-based specifications.The Journal of Software Testing,Verification,and Reliability,13(1):25-53,March 2003.
[53]Wagner,F.,"Modeling Software with Finite State Machines:A Practical Approach",Auerbach Publications,2006,ISBN 0-8493-8086-3.
[54]D.Raggett,A.Le Hors,and I.Jacobs.HTML 4.01 specification.W3C recommendation,W3C,http://www.w3.org/TR/1999/REC-html401-19991224/,1997-1999.
[55]Paul Ammann and Jeff Offutt.Coverage Criteria for Software Testing.In preparation,2004.
[56]T.Chow.Testing software designs modeled by finite-state machines.IEEE Transactions on Software Engineering,SE-4(3):178{187,May 1978.
[57]S.Fujiwara,G.Bochmann,F.Khendek,M.Amalou,and A.Ghedasmi.Test selection based on finite state models.IEEE Transactions on Software Engineering,17(6):591{603,June 1991.
[58]Jeff Offutt,Shaoying Liu,Aynur Abdurazik,and Paul Ammann.Generating test data from state-based specifications.The Journal of Software Testing,Verification,and Reliability,13(1):25{53,March 2003.
[59]曾红卫.Wleb应用的验证与测试方法研究.博士学位论文.2008.02.
[60]Kung D C,Liu C H,Hsia P.An Object-Oriented Web Test Model for Testing Web Applications[C]//Proceedings of the 1st Asia-Pacific Conference on Web Applications (APAQS 2000),Washington:IEEE Computer Society,2000:111-120.
[61]Van Beck H M A,Mauw S.Automatic conformance testing of internet applications.Formal Approaches to Software Testing-FATES 2003,Lecture Notes in Computer Science.Germany:Springer-Verlag,2004:53-63.
[62]Leung,K.R.,Hui,L.C.,Yiu,S.M.,and Tang,R.W.2000.Modeling Web Navigation by Statechart.In 24th international Computer Software and Applications Conference(October 25-28,2000).COMPSAC.IEEE Computer Society,Washington,DC,41-47.
[63]Ricca,F.and Tonella,P.2001.Analysis and testing of Web applications.In Proceedings of the 23rd international Conference on Software Engineering(Toronto,Ontario,Canada,May 12-19,2001).International Conference on Software Engineering.IEEE Computer Society,Washington,DC,25-34.
[64]M.Haydar,A.Petrenko,and H.Sahraoui,"Formal Verification of Web Applications Modeled by Communicating Automata",in Proe.of 24th IFIP WG 6.1 IFIP Int.Conference on Formal Techniques for Networked and Distributed Systems(FORTE 2004),LNCS,vol.3235,pp.115-132,Madrid,Spain,September 2004.
[65]Donini FM,Mongiello M,Ruta M,and Totaro R.A Model Checking-based Method for Verifying Web Application Design.Electronic Notes in Theoretical Computer Science,151(2),2006,pp.19-32.
[66]Han,M.and Hofmeister,C.2006.Modeling and verification of adaptive navigation in web applications.In Proceedings of the 6th international Conference on Web Engineering(Palo Alto,California,USA,July 11-14,2006).ICWE '06,vol.263.ACM,New York,NY,329-336.
[67]Jim Conallen.Building Web Applications with UML(Second Edition).Addison Wesley,Inc.2002.
[68]Bellettini,C.,Marchetto,A.,and Trentini,A.2004.WebUml:reverse engineering of web applications.In Proceedings of the 2004 ACM Symposium on Applied Computing(Nicosia,Cyprus,March 14-17,2004).SAC '04.ACM,New York,NY,1662-1669.
[69]M.Haydar,A.Petrenko,and H.Sahraoui,"Formal Verification of Web Applications Modeled by Communicating Automata",in Proc.of 24th IFIP WG 6.1 IFIP Int.Conference on Formal Techniques for Networked and Distributed Systems(FORTE 2004),LNCS,vol.3235,pp.115-132,Madrid,Spain,September 2004.
[70]Schwabe,D.,de Almeida Pontes,R.,and Moura,I.1999.OOHDM-Web:an environment for implementation of hypermedia applications in the WWW.SIGWEB Newsl.8,2(Jun.1999),18-34.
[71]T.Isakowitz,E.A.Stohr,and P.Balasubramanian,"RMM:A Methodology for Structured Hypermedia Design",Communications of the ACM,Vol.38,No.8,August 1995,pp.34-44.
[72]L.Tauscher,and S.Greenberg,"Design Guidelines for Effective WWW History Mechanisms",In Proceedings of the 2nd Conference on Human Factors and the Web:Designing for the Web-Empirical Studies,In Microsoft Workshop,Microsoft Corporation,Redmond,WA,Oct.1996.
[73]G.A.D.Lucca,and M.D.Penta,"Considering Browser Interaction in Web Application Testing",In Proceedings of the 5th IEEE International Workshop on Web Site Evolution,IEEE Press,New York,USA,2003,pp.74-81.
[74]A.Cockbum,and S.Jones,"Which Way Now? Analyzing and Easing Inadequacies in WWW Navigation",International Journal of Human-Computer Studies,Vol.45,No.1,1996,pp.105-129.
[75]S.Greenberg,and A.Cockburn,"Getting Back to Back:Alternate Behaviors for a Web Browser's Back Button",In Proceedings of 5th Conference on Annual Human Factors and the Web,Gaithersburg,Maryland,USA,Jun.1999.
[76]J.Nielsen,Hypertext and Hypermedia,Academic Press Professional,Inc.,San Diego,CA,USA,1990.
[77]J.Chen,and X.S.Zhao,"Formal Models for Web Navigations with Session Control and Browser Cache",J.Davies et al.(Eds.),ICFEM 2004,LNCS 3308,Springer-Verlag,2004,pp.46-60.
[78]K.L.McMillan,"The SMV System for SMV version 2.5.4",http://www.cs.cmu.edu /～modelcheck/smv/-smvmanual.ps,October,2006.
[79]E.Di Sciascio,F.M.Donini,M.Mongiello,and G.Piscitelli.Web Applications Design and aintenance using Symbolic Model Checking.In Proc.of CSMR '03,pp.63-72,Benevento, Italy,March 26-28 2003.IEEE.
[80]M.A.S.Turine,M.C.F.Oliveira,and P.C.Masiero,"A Navigation-oriented Hypertext Model Based on Statecharts",In Proceedings of the 8th ACM Conference on Hypertext (Hypertext'97),Southamption,UK,1997,pp.102-111.
[81]K.R.P.H.Leung,L.C.K.Hui,and S.M.Yiu et al.,"Modeling Web Navigation by Statechart",In Proceedings of the 24th Annual International Computer Software and Applications Conference(COMPSAC 2000),Oct.2000,pp.41-47.
[82]M.Cristina and F.De Oliviera,"A Statechart-based Model for Hypermedia Applications",ACM Transactions on Information Systems,Vol.19,No.1,Jan.2001,pp.28-52.
[83]J.Dargham and S.AI-Nasrawi,"FSM Behavioral Modeling Approach for Hypermedia Web Applications:FBM-HWA Approach",In Proceedings of the Advanced International Conference on Telecommunications and International Conference on Internet and Web Applications and Services(AICT/ICIW 2006),Guadeloupe,Caribbean,French,2006,pp.199-204.
[84]Takano,H.and Winograd,T.1998.Dynamic bookmarks for the WWW.In Proceedings of the Ninth ACM Conference on Hypertext and Hypermedia:Links,Objects,lime and Space—Structure in Hypermedia Systems:Links,Objects,Time and Space—Structure in Hypermedia Systems(Pittsburgh,Pennsylvania,United States,June 20-24,1998).HYPERTEXT'98.ACM,New York,NY,297-298.
[85]Li,W.,Vu,Q.,Agrawal,D.,Hara,Y.,and Takano,H.1999.PowerBookmarks:a system for personalizable Web information organization,sharing,and management.In Proceedings of the Eighth international Conference on World Wide Web(Toronto,Canada).P.H.Enslow,Ed.Elsevier North-Holland,New York,NY,1375-1389.
[86]Miao,H.,Qian,Z.,and He,T.2007.Modeling Web Browser Interactions Using FSM.In Proceedings of the the 2nd IEEE Asia-Pacific Service Computing Conference(December 11-14,2007).APSCC.IEEE Computer Society,Washington,DC,pp.211-217.
[87]Miao,H.and Zeng,H.2007.Model Checking-based Verification of Web Application.In Proceedings of the 12th IEEE international Conference on Engineering Complex Computer Systems(ICECCS 2007)(July 11-14,2007).ICECCS.IEEE Computer Society,Washington,DC,pp.47-55.
[88]F.M.Donini,M.Mongiello,M.Ruta,and R.Totaro,"A Model Checking-based Method for Verifying Web Application Design",Electronic Notes in Theoretical Computer Science,151(2),2006,pp.19-32.
[89]Han,M.and Hofmeister,C.2006.Modeling and verification of adaptive navigation in web applications.In Proceedings of the 6th international Conference on Web Engineering(Palo Alto,California,USA,July 11-14,2006).ICWE '06,vol.263.ACM,New York,NY,pp.329-336.
[90]T.Chow.Testing software designs modeled by finite-state machines.IEEE Transactions on Software Engineering,SE-4(3):178-187,May 1978.
[91]S.Fujiwara,G.Bochmann,F.Khendek,M.Amalou,and A.Ghedasmi.Test selection based on finite state models.IEEE Transactions on Software Engineering,17(6):591-603,June 1991.
[92]Jeff Offutt,Shaoying Liu,Aynur Abdurazik,and Paul Ammann.Generating test data from state-based specifications.The Journal of Software Testing,Verification,and Reliability,13(1):25-53,March 2003.
[93]A.Andrews,J.Offutt and R.Alexander.Testing Web Applications by Modeling with FSMs,Software Systems and Modeling,4(3),August 2005.
[94]Timothy J.Grose,Gary C.Doney,Stephen A.Brodsky.Mastering XMI Java Programming with XMI,XML,and UML.John Wiley & Sons,Inc.2002
[95]XML Metadata Interchange(XMI),v2.1.1,http://www.omg.org/technology/documents /formal/xmi.htm
[96]Rational Rose 2007,http://www-306.ibm.com/software/awdtools/developer/rose/
[97]ArgoUML0.25.4,http://argouml.tigris.org/
[98]MagicDraw UML,http://www.magicdraw.com/
[99]Lombardy S.,R'egis-Gianas Y.,and Sakarovitch J.,Introducing Vaucanson Theoretical Comput.Sci.328(2004),77-96.Journal version of Proc.of CIAA 2003,Lect.Notes in Comp.Sc.2759,(2003),96-107(with R.Poss).
[100]http://www.lrde.epita.fr/cgi-bin/twiki/view/Projects/Vaucanson
[101]Claveirole T.,Proposal:an XML representation for automata,Technical report,LRDE (2004).
[102]http://robotflow.sourceforge.net/documents/FSMDescription.pdf
[2]Grady Booch,James Rumbaugh,Ivar Jacobson.Unified Modeling Language User Guide,2nd Edition).Addison-Wesley,2005.
[3]James Rumbaugh,Ivar Jacobson,Grady Booch.Unified Modeling Language Reference Manual(2nd Edition).Addison-Wesley,Jul 19,2004.
[4]Jim Conallen,Building Web Applications with UML,Second Edition,Addison Wesley,2002.
[5]Alfred V.Aho,Ravi Sethi,Jeffrey D.Ullman and Monica S.Lam.Compilers:Principles,Techniques,and Tools(second edition).Addison-Wesley,Inc.2006.
[6]张素琴,吕映芝,蒋维杜,戴桂兰.编译原理(第2版).清华大学出版社.2005.
[7]Holzmann G.J..The model checker SPIN.IEEE Transactions on Software Engineering,1997,23(5):279-295.
[8]Vardi,M.Y.2001.Branching vs.Linear Time:Final Showdown.In Proceedings of the 7th international Conference on Tools and Algorithms For the Construction and Analysis of Systems(April 02-06,2001).T.Margaria and W.Yi,Eds.Lecture Notes In Computer Science,vol.2031.Springer-Verlag,London,1-22.
[9]McMillan KL.The SMV System for SMV version 2.5.4.http://www.cs.cmu.edu/～modelcheck/smv/smvmanual.ps,October,2006.
[10]Huth M and Ryan M.Logic in Computer Science:Modelling and Reasoning about Systems.Cambridge University Press,2004,170-255.
[11]Pnueli A.The temporal semantics of concurrent programs.Theoretical Computer Science,1981,13:45-60.
[12]Clarke EM and Emerson E A,and Sistla AP.Automatic verification of finite-state concurrent systems using temporal logic specifications.ACM Transactions on Programming Languages and Systems,1986,8(2):244-263.
[13]Clarke EM and Emerson E A.Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic.In Logic of Programs:Workshop,Yorktown Heights,NY,LNCS131.Springer-Verlag,1981:52-71.
[14]Browne M C,Clarke EM,Dill D L,Mishra B.Automatic verification of asynchronous circuits using temporal logic.IEEE Transactions on Computers,1986,35(12):1035-1044.
[15]Queille,J.and Sifakis,J.1982.Specification and verification of concurrent systems in CESAR.In Proceedings of the 5th Colloquium on international Symposium on Programming (April 06-08,1982).M.Dezani-Ciancaglini and U.Montanari,Eds.Lecture Notes In Computer Science,vol.137.Springer-Verlag,London,337-351.
[16]Sistla AP and Clarke EM.Complexity of Propositional temporal logics.Jonrnal of the ACM,1985,32(3):733-749.
[17]Lichtenstein O,Pnueli A.Checking that finite state concurrent programs satisfy their linear specification.In:Proceedings of the 12th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages,New York,1985,97-107.
[18]McMillan KL.The SMV System for SMV version 2.5.4.http://www.cs.cmu.edu/～modelcheck/smv/smvmanual.ps,October,2006.
[19]Huth M and Ryan M.Logic in Computer Science:Modelling and Reasoning about Systems.Cambridge University Press,2004,170-255.
[20]Burch JR,Clarke EM,MeMillan KL,Dill DL,Hwang LJ.Symbolic model checking:1020states and beyond.Information and Computation,1992,98(2):142-170.
[21]Bryant R E.Symbolic Boolean manipulation with ordered binary decision diagrams.ACM Computing Surveys,1992,24(3):293-318.
[22] Biere A, Cimatti A, Clarke EM, and Zhu Y. Symbolic model checking without BDDs. In TACAS '99: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, London, UK. 1999,193-207.
[23] Courcoubetis C, Vardi M, Wolper P, and Yannakakis M. Memory efficient algorithms for the verification of temporal properties. In: Proc, of the 2nd International Workshop on Computer Aided Verification(CAV90), 1990,233-242.
[24] Alur R, Brayton RK, Henzinger TA, Qadeer S, Rajamani SK. Partial-Order reduction in symbolic state space exploration. In: Proc.of the 9th Int'l Conf, on Computer Aided Verification. LNCS 1254, Grumberg, springer-Verlag, 1997. 340-351.
[25] Berezin, S., Campos, S. V, and Clarke, E. M. 1998. Compositional Reasoning in Model Checking. In Revised Lectures From the international Symposium on Compositionality: the Significant Difference (September 08-12, 1997). W. P. Roever, H. Langmaack, and A. Pnueli, Eds. Lecture Notes In Computer Science, vol. 1536. Springer-Verlag, London, 81-102.
[26] Henzinger TA, Qadeer S, Rajamani SK, Tasiran S. An assume-guarantee rule for checking simulation. ACM Trans, on Programming Languages and Systems, 2002,24(1):51-64.
[27] Dams D. Abstraction in software model checking: Principles and practice (tutorial overview and bibliography ). Model Checking Software. Vol LNCS2318, Springer-Verlag, 2002, 53-67.
[28] Park D. Concurrency and automata on infinite sequences. In: 5th GI-Conference on Theoretical Computer Science. Berlin:Springer, 1981,167-183.
[29] Ball T, Majumdar R, Millstein T, and Rajamani SK. Automatic predicate abstraction of C programs. ACM SIGPLAN Notices, 2001, 36(5): 203-213.
[30] Graf S, Saidi H. Construction of abstract state graphs with PVS.In: Orna Grumberg, ed. Proceedings of the 9th International Conference on Computer Aided Verification (CAV '97), LNCS 1254, Springer-Verlag,1997,72-83.
[31] Ball T, Rajamani SK. Automatically validating temporal safety properties of interfaces. In: Matthew B D, ed. Proc of the 8th International SPIN Workshop on Model Checking of Software, LNCS 2057, Heidelberg: Springer-Verlag, 2001. 103-122.
[32] Henzinger TA, Jhala R, Majumdar R, and Sutre G Lazy abstraction. In: Proc, of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Langauges (POPL'02), ACM SIGPLAN Notices, ACM, 2002, 37(1): 58-70.
[33] Corbett JC, Dwyer MB, Hatcli J, PasSreanu CS, Robby, Laubach S, and Zheng H. Bandera: extracting finite-state models from Java source code. In: Proc, of the 22nd International Conference on Software Engineering (ICSE '00), IEEE Computer Society Press, 2000. 439-448.
[34] Clarke E M, Grumberg O, Long D E. Model checking and abstraction. ACM Transactions on Programming Languages and System, 1994,16 (5):1512-1542.
[35] Clarke E, Grumberg O, Jha S, Lu Y, and Veith H. Counterexample-guided abstraction refinement. In: Proc, of International Conference on Computer Aided Verification (CAV00), LNCS 1855, Heidelberg: Springer-Verlag, 2000. 154-169.
[36] Chaki S, Clarke E M, Groce A, Jha S, and Veith H. Modular verification of software components in C. IEEE Transactions on Software Engineering, 2004, 30(6): 388-402.
[37] Godefroid P. Software model checking: the Verisoft approach. Formal Method in System Design, Kluwer Academic Publishers, 2005, 26(2):77-101.
[38] Havelund K and Pressburger T. Model checking Java programs using Java PathFinder. Software Tools for Technology Transfer, 1998,2(4): 366-381.
[39] [~1] Hong HS, Lee I, Sokolsky O, and Cha SD. Automatic test generation from Statecharts using model checking. In: Proceedings of the 1st International Workshop on Formal Approaches to Testing of Software (FATES '01), Aalborg, Denmark, Aug. 2001,15-30.
[40] Ammann PE and Black PE. Test generation and recognition with formal methods. In Intl. Workshop on Automated Program Analysis, Testing and Verification, Limerick, Ireland, 2000, 64-67.
[41] Gargantini A and Heitmeyer C. Using model checking to generate tests from requirements specifications. In ESEC '99, LNCS 1687, Springer-Verlag, 1999:146-162.
[42]Rene de Vries,Jan Tretmans.On-the-fly conformance testing using SPIN.Software Tools for Technology Transfer,2000,2(4):382-393.
[43]Hong,H.S.,Lee,I.,Sokolsky,O.,and Ural,H.2002.A Temporal Logic Based Theory of Test Coverage and Generation.In Proceedings of the 8th international Conference on Tools and Algorithms For the Construction and Analysis of Systems(April 08-12,2002).J.Katoen and P.Stevens,Eds.Lecture Notes In Computer Science,vol.2280.Springer-Verlag,London,327-341.
[44]Hong HS,Cha S D,Lee I,et al.Data flow testing as model checking.In:Proceedings of 25th International Conference on Software Engineering.Washington:IEEE Computer Society,2003:232-242.
[45]Ammann,P.E.,Black,P.E.,and Majurski,W.1998.Using Model Checking to Generate Tests from Specifications.In Proceedings of the Second IEEE international Conference on Formal Engineering Methods(December 09-11,1998).ICFEM.IEEE Computer Society,Washington,DC,46-54.
[46]Rajah,S.,Shankar,N.,and Srivas,M.K.1995.An Integration of Model Checking with Automated Proof Checking.In Proceedings of the 7th international Conference on Computer Aided Verification(July 03-05,1995).P.Wolper,Ed.Lecture Notes In Computer Science,vol.939.Springer-Verlag,London,84-97.
[47]Manna Z,Sipma H.Deductive Verification of Hybrid Systems Using SteP.HSCC 1998,305-318.
[48]R.V.Binder.Testing Object-Oriented Systems:Models,Patterns,and Tools.Addison-Wesley,2000.
[49]Chow,T.S.1978.Testing Software Design Modeled by Finite-State Machines.IEEE Trans.Softw.Eng.4,3(May.1978),178-187.
[50]T.Chow.Testing software designs modeled by finite-state machines.IEEE Transactions on Software Engineering,SE-4(3):178-187,May 1978.
[51]S.Fujiwara,G.Bochmann,F.Khendek,M.Amalou,and A.Ghedasmi.Test selection based on finite state models.IEEE Transactions on Software Engineering,17(6):591-603,June 1991.
[52]J.Offutt,S.Liu,A.Abdurazik,and P.Ammann.Generating test data from state-based specifications.The Journal of Software Testing,Verification,and Reliability,13(1):25-53,March 2003.
[53]Wagner,F.,"Modeling Software with Finite State Machines:A Practical Approach",Auerbach Publications,2006,ISBN 0-8493-8086-3.
[54]D.Raggett,A.Le Hors,and I.Jacobs.HTML 4.01 specification.W3C recommendation,W3C,http://www.w3.org/TR/1999/REC-html401-19991224/,1997-1999.
[55]Paul Ammann and Jeff Offutt.Coverage Criteria for Software Testing.In preparation,2004.
[56]T.Chow.Testing software designs modeled by finite-state machines.IEEE Transactions on Software Engineering,SE-4(3):178{187,May 1978.
[57]S.Fujiwara,G.Bochmann,F.Khendek,M.Amalou,and A.Ghedasmi.Test selection based on finite state models.IEEE Transactions on Software Engineering,17(6):591{603,June 1991.
[58]Jeff Offutt,Shaoying Liu,Aynur Abdurazik,and Paul Ammann.Generating test data from state-based specifications.The Journal of Software Testing,Verification,and Reliability,13(1):25{53,March 2003.
[59]曾红卫.Wleb应用的验证与测试方法研究.博士学位论文.2008.02.
[60]Kung D C,Liu C H,Hsia P.An Object-Oriented Web Test Model for Testing Web Applications[C]//Proceedings of the 1st Asia-Pacific Conference on Web Applications (APAQS 2000),Washington:IEEE Computer Society,2000:111-120.
[61]Van Beck H M A,Mauw S.Automatic conformance testing of internet applications.Formal Approaches to Software Testing-FATES 2003,Lecture Notes in Computer Science.Germany:Springer-Verlag,2004:53-63.
[62]Leung,K.R.,Hui,L.C.,Yiu,S.M.,and Tang,R.W.2000.Modeling Web Navigation by Statechart.In 24th international Computer Software and Applications Conference(October 25-28,2000).COMPSAC.IEEE Computer Society,Washington,DC,41-47.
[63]Ricca,F.and Tonella,P.2001.Analysis and testing of Web applications.In Proceedings of the 23rd international Conference on Software Engineering(Toronto,Ontario,Canada,May 12-19,2001).International Conference on Software Engineering.IEEE Computer Society,Washington,DC,25-34.
[64]M.Haydar,A.Petrenko,and H.Sahraoui,"Formal Verification of Web Applications Modeled by Communicating Automata",in Proe.of 24th IFIP WG 6.1 IFIP Int.Conference on Formal Techniques for Networked and Distributed Systems(FORTE 2004),LNCS,vol.3235,pp.115-132,Madrid,Spain,September 2004.
[65]Donini FM,Mongiello M,Ruta M,and Totaro R.A Model Checking-based Method for Verifying Web Application Design.Electronic Notes in Theoretical Computer Science,151(2),2006,pp.19-32.
[66]Han,M.and Hofmeister,C.2006.Modeling and verification of adaptive navigation in web applications.In Proceedings of the 6th international Conference on Web Engineering(Palo Alto,California,USA,July 11-14,2006).ICWE '06,vol.263.ACM,New York,NY,329-336.
[67]Jim Conallen.Building Web Applications with UML(Second Edition).Addison Wesley,Inc.2002.
[68]Bellettini,C.,Marchetto,A.,and Trentini,A.2004.WebUml:reverse engineering of web applications.In Proceedings of the 2004 ACM Symposium on Applied Computing(Nicosia,Cyprus,March 14-17,2004).SAC '04.ACM,New York,NY,1662-1669.
[69]M.Haydar,A.Petrenko,and H.Sahraoui,"Formal Verification of Web Applications Modeled by Communicating Automata",in Proc.of 24th IFIP WG 6.1 IFIP Int.Conference on Formal Techniques for Networked and Distributed Systems(FORTE 2004),LNCS,vol.3235,pp.115-132,Madrid,Spain,September 2004.
[70]Schwabe,D.,de Almeida Pontes,R.,and Moura,I.1999.OOHDM-Web:an environment for implementation of hypermedia applications in the WWW.SIGWEB Newsl.8,2(Jun.1999),18-34.
[71]T.Isakowitz,E.A.Stohr,and P.Balasubramanian,"RMM:A Methodology for Structured Hypermedia Design",Communications of the ACM,Vol.38,No.8,August 1995,pp.34-44.
[72]L.Tauscher,and S.Greenberg,"Design Guidelines for Effective WWW History Mechanisms",In Proceedings of the 2nd Conference on Human Factors and the Web:Designing for the Web-Empirical Studies,In Microsoft Workshop,Microsoft Corporation,Redmond,WA,Oct.1996.
[73]G.A.D.Lucca,and M.D.Penta,"Considering Browser Interaction in Web Application Testing",In Proceedings of the 5th IEEE International Workshop on Web Site Evolution,IEEE Press,New York,USA,2003,pp.74-81.
[74]A.Cockbum,and S.Jones,"Which Way Now? Analyzing and Easing Inadequacies in WWW Navigation",International Journal of Human-Computer Studies,Vol.45,No.1,1996,pp.105-129.
[75]S.Greenberg,and A.Cockburn,"Getting Back to Back:Alternate Behaviors for a Web Browser's Back Button",In Proceedings of 5th Conference on Annual Human Factors and the Web,Gaithersburg,Maryland,USA,Jun.1999.
[76]J.Nielsen,Hypertext and Hypermedia,Academic Press Professional,Inc.,San Diego,CA,USA,1990.
[77]J.Chen,and X.S.Zhao,"Formal Models for Web Navigations with Session Control and Browser Cache",J.Davies et al.(Eds.),ICFEM 2004,LNCS 3308,Springer-Verlag,2004,pp.46-60.
[78]K.L.McMillan,"The SMV System for SMV version 2.5.4",http://www.cs.cmu.edu /～modelcheck/smv/-smvmanual.ps,October,2006.
[79]E.Di Sciascio,F.M.Donini,M.Mongiello,and G.Piscitelli.Web Applications Design and aintenance using Symbolic Model Checking.In Proc.of CSMR '03,pp.63-72,Benevento, Italy,March 26-28 2003.IEEE.
[80]M.A.S.Turine,M.C.F.Oliveira,and P.C.Masiero,"A Navigation-oriented Hypertext Model Based on Statecharts",In Proceedings of the 8th ACM Conference on Hypertext (Hypertext'97),Southamption,UK,1997,pp.102-111.
[81]K.R.P.H.Leung,L.C.K.Hui,and S.M.Yiu et al.,"Modeling Web Navigation by Statechart",In Proceedings of the 24th Annual International Computer Software and Applications Conference(COMPSAC 2000),Oct.2000,pp.41-47.
[82]M.Cristina and F.De Oliviera,"A Statechart-based Model for Hypermedia Applications",ACM Transactions on Information Systems,Vol.19,No.1,Jan.2001,pp.28-52.
[83]J.Dargham and S.AI-Nasrawi,"FSM Behavioral Modeling Approach for Hypermedia Web Applications:FBM-HWA Approach",In Proceedings of the Advanced International Conference on Telecommunications and International Conference on Internet and Web Applications and Services(AICT/ICIW 2006),Guadeloupe,Caribbean,French,2006,pp.199-204.
[84]Takano,H.and Winograd,T.1998.Dynamic bookmarks for the WWW.In Proceedings of the Ninth ACM Conference on Hypertext and Hypermedia:Links,Objects,lime and Space—Structure in Hypermedia Systems:Links,Objects,Time and Space—Structure in Hypermedia Systems(Pittsburgh,Pennsylvania,United States,June 20-24,1998).HYPERTEXT'98.ACM,New York,NY,297-298.
[85]Li,W.,Vu,Q.,Agrawal,D.,Hara,Y.,and Takano,H.1999.PowerBookmarks:a system for personalizable Web information organization,sharing,and management.In Proceedings of the Eighth international Conference on World Wide Web(Toronto,Canada).P.H.Enslow,Ed.Elsevier North-Holland,New York,NY,1375-1389.
[86]Miao,H.,Qian,Z.,and He,T.2007.Modeling Web Browser Interactions Using FSM.In Proceedings of the the 2nd IEEE Asia-Pacific Service Computing Conference(December 11-14,2007).APSCC.IEEE Computer Society,Washington,DC,pp.211-217.
[87]Miao,H.and Zeng,H.2007.Model Checking-based Verification of Web Application.In Proceedings of the 12th IEEE international Conference on Engineering Complex Computer Systems(ICECCS 2007)(July 11-14,2007).ICECCS.IEEE Computer Society,Washington,DC,pp.47-55.
[88]F.M.Donini,M.Mongiello,M.Ruta,and R.Totaro,"A Model Checking-based Method for Verifying Web Application Design",Electronic Notes in Theoretical Computer Science,151(2),2006,pp.19-32.
[89]Han,M.and Hofmeister,C.2006.Modeling and verification of adaptive navigation in web applications.In Proceedings of the 6th international Conference on Web Engineering(Palo Alto,California,USA,July 11-14,2006).ICWE '06,vol.263.ACM,New York,NY,pp.329-336.
[90]T.Chow.Testing software designs modeled by finite-state machines.IEEE Transactions on Software Engineering,SE-4(3):178-187,May 1978.
[91]S.Fujiwara,G.Bochmann,F.Khendek,M.Amalou,and A.Ghedasmi.Test selection based on finite state models.IEEE Transactions on Software Engineering,17(6):591-603,June 1991.
[92]Jeff Offutt,Shaoying Liu,Aynur Abdurazik,and Paul Ammann.Generating test data from state-based specifications.The Journal of Software Testing,Verification,and Reliability,13(1):25-53,March 2003.
[93]A.Andrews,J.Offutt and R.Alexander.Testing Web Applications by Modeling with FSMs,Software Systems and Modeling,4(3),August 2005.
[94]Timothy J.Grose,Gary C.Doney,Stephen A.Brodsky.Mastering XMI Java Programming with XMI,XML,and UML.John Wiley & Sons,Inc.2002
[95]XML Metadata Interchange(XMI),v2.1.1,http://www.omg.org/technology/documents /formal/xmi.htm
[96]Rational Rose 2007,http://www-306.ibm.com/software/awdtools/developer/rose/
[97]ArgoUML0.25.4,http://argouml.tigris.org/
[98]MagicDraw UML,http://www.magicdraw.com/
[99]Lombardy S.,R'egis-Gianas Y.,and Sakarovitch J.,Introducing Vaucanson Theoretical Comput.Sci.328(2004),77-96.Journal version of Proc.of CIAA 2003,Lect.Notes in Comp.Sc.2759,(2003),96-107(with R.Poss).
[100]http://www.lrde.epita.fr/cgi-bin/twiki/view/Projects/Vaucanson
[101]Claveirole T.,Proposal:an XML representation for automata,Technical report,LRDE (2004).
[102]http://robotflow.sourceforge.net/documents/FSMDescription.pdf