基于接口自动机的服务组合验证研究
|
摘要
目前,随着Web服务技术的不断推广与应用,面向服务的计算已经成为软件工程领域的研究热点。通过重用现有服务,将服务进行组合,企业能够更为快速有效的构建具有灵活、松耦合特点的分布式系统。如何利用现有的服务资源,搭建结构更复杂,功能更强大的业务系统,以及验证服务组合与业务需求的一致性,是当前研究的一个重点。
针对目前缺乏一种支持图形化表示、形式化验证的服务组合模型,本文提出了基于接口自动机的服务组合模型,该模型扩展了接口自动机,能够同时描述服务流程与服务语义。本文设计了BPEL流程到接口自动机模型的转换算法。模型利用接口自动机并发组合算法实现服务流程的组合,通过检测接口自动机的行为模型来验证服务流程与业务需求的一致性。实验表明,基于接口自动机的服务组合模型能够准确、完备的表达BPEL流程,同时模型能够准确的验证服务流程与业务流程是否一致。
针对目前缺乏一种对服务质量(QoS)需求的验证方法,本文在接口自动机模型的基础上,提出了一种对服务QoS需求进行验证的方法。该方法在将服务质量属性进行定量描述的基础上,设计了一种针对QoS需求的形式化表述策略。针对BPEL对QoS属性支持不足的缺点,在BPEL上扩展了描述QoS属性的标签。本方法能对由接口自动机模型组合后的组合服务中每一项业务功能均进行QoS需求验证,通过和其他QOS验证方法实验比较,本方法能够更高效的验证QoS需求。
本文主要关注于服务组合验证方面的研究,包括接口自动机的服务组合模型、组合服务与业务功能一致性的验证以及QoS需求验证。对以上问题提出了有效的解决方案,对于推进Web服务组合与验证技术的理论研究提供了新思路和方法。
Nowadays, with the constant development of Web services technology, service-oriented computing has become a research hotspot of software engineering. By reusing the existing services to combine the service, it can make the enterprises to build flexible and loose-coupled distributed systems more efficiently and effectively. How to make use of the existing service to build an business system which is more complicated and more powerful and to verify the consistency of service combination and business requirment is our key research currently.
To solve the problem that there is no such a model which can support graphical display and formalized variation of the service composition, this paper presents a service composition model based on the interface automata to extend the automata. Meanwhile, the model describes service operation and service semantics. The paper designs a transformation algorithm from BPEL process to interface automata model. The model uses composition of interface automata to execute the composition of service. By the way of testing the behavior model of interface automata to verify the consistency of service and business requirements. Experiments have approved that service combination model based on interface automata can express BPEL procedure accurately and completely. It can verify the consistency of service procedure and business procedure.
To the question of lack of verified method based on Qos needs, this article presents a model building method to verify the QoS requirements on the basis of interface automata. Except quantitative describing the service quality attribute, the method also designs a formalized expression aiming at Qos requirements. To avoid the shortcoming of BPEL's inefficient support to QoS attributes, it designs a label to describe QoS attributes in BPEL. This method will do QoS needs verification for each operation service after the combination of the interface automata model, comparing with other QoS verification methods. It can verify Qos requirements efficiently.
This paper focuses on the research of the services composition and services verification, including service composition model of interface automata, the consistency verification between service composition and business function and the verification of QoS requirements. These are effective attempt research and provide new ideas and methods for the further research on the technology of Web services composition and verification.
针对目前缺乏一种支持图形化表示、形式化验证的服务组合模型,本文提出了基于接口自动机的服务组合模型,该模型扩展了接口自动机,能够同时描述服务流程与服务语义。本文设计了BPEL流程到接口自动机模型的转换算法。模型利用接口自动机并发组合算法实现服务流程的组合,通过检测接口自动机的行为模型来验证服务流程与业务需求的一致性。实验表明,基于接口自动机的服务组合模型能够准确、完备的表达BPEL流程,同时模型能够准确的验证服务流程与业务流程是否一致。
针对目前缺乏一种对服务质量(QoS)需求的验证方法,本文在接口自动机模型的基础上,提出了一种对服务QoS需求进行验证的方法。该方法在将服务质量属性进行定量描述的基础上,设计了一种针对QoS需求的形式化表述策略。针对BPEL对QoS属性支持不足的缺点,在BPEL上扩展了描述QoS属性的标签。本方法能对由接口自动机模型组合后的组合服务中每一项业务功能均进行QoS需求验证,通过和其他QOS验证方法实验比较,本方法能够更高效的验证QoS需求。
本文主要关注于服务组合验证方面的研究,包括接口自动机的服务组合模型、组合服务与业务功能一致性的验证以及QoS需求验证。对以上问题提出了有效的解决方案,对于推进Web服务组合与验证技术的理论研究提供了新思路和方法。
Nowadays, with the constant development of Web services technology, service-oriented computing has become a research hotspot of software engineering. By reusing the existing services to combine the service, it can make the enterprises to build flexible and loose-coupled distributed systems more efficiently and effectively. How to make use of the existing service to build an business system which is more complicated and more powerful and to verify the consistency of service combination and business requirment is our key research currently.
To solve the problem that there is no such a model which can support graphical display and formalized variation of the service composition, this paper presents a service composition model based on the interface automata to extend the automata. Meanwhile, the model describes service operation and service semantics. The paper designs a transformation algorithm from BPEL process to interface automata model. The model uses composition of interface automata to execute the composition of service. By the way of testing the behavior model of interface automata to verify the consistency of service and business requirements. Experiments have approved that service combination model based on interface automata can express BPEL procedure accurately and completely. It can verify the consistency of service procedure and business procedure.
To the question of lack of verified method based on Qos needs, this article presents a model building method to verify the QoS requirements on the basis of interface automata. Except quantitative describing the service quality attribute, the method also designs a formalized expression aiming at Qos requirements. To avoid the shortcoming of BPEL's inefficient support to QoS attributes, it designs a label to describe QoS attributes in BPEL. This method will do QoS needs verification for each operation service after the combination of the interface automata model, comparing with other QoS verification methods. It can verify Qos requirements efficiently.
This paper focuses on the research of the services composition and services verification, including service composition model of interface automata, the consistency verification between service composition and business function and the verification of QoS requirements. These are effective attempt research and provide new ideas and methods for the further research on the technology of Web services composition and verification.
引文
[1]W3C.Web Sevrices Acrhitecutre[Z],2004. http://www.w3.org/TR/2004/NOTE-ws-arch-20040211
[2]Michael P. Papazoglou, Paolo Traverso, Schahran Dustdar, et al. Service-Oriented Computing:State of the Art and Research Challenges. Computer,2007,40(11):38-45
[3]M.P.Papazoglou, D.Georgakopoulous. Service-Oriented Computing. Communication of the ACM,2003,46(10):25-28
[4]SOAP Specifications.http://www.w3.org/TR/soap
[5]Web Services Description Language. http://www.w3.org/TR/wsdl
[6]Andrews T, Curbera F, et al. Business Process Execution Language for Web Servic e (BPEL4WS) 1.1,2003. http://www.ibm.com/developerworks/library/ws-bpel/.
[7]Resource Description Framework. http://www.w3.org/RDF/
[8]OWL Web Ontology Language Guide.http://www.w3.org/TR/2004/REC-owl-guide-20040210
[9]雷丽晖,段振华.一种基于扩展有限自动机验证组合Web服务的方法,Journal of Software, Vol.18, No.12, December 2007
[10]王晨,王红兵,许迅.一种验证Web服务流程的新方法,计算机应用研究,2008,第25卷第12期
[11]苏焕程,黄志球,刘林源.基于接口自动机的BPEL4WS+Web服务组合形式化模型,计算机应用研究,2009年第5期
[12]D Chenthati, S Vaddi, H Mohanty. Verification of Web Services Modeled as Finite State Machines. In:2010 Fourth Asia International Conference on Mathematical/Analytical Modelling and Computer Simulation
[13]Tao Liu, Guosun Zeng, Adaptation of Mismatching Services Based on Labelled Interface Automata. In:2009 Fifth International Conference on Semantics, Knowledge and Grid
[14]Tevfik Bultan,Xiang Fu,Richard Hull,Jianwen Su. An Interface Automata based Model for Web Service Composition. In:12th international conference on World Wide Web ACM New York, NY, USA 2003
[15]Tao Liu,Guosun Zeng. Detecting and Resolving Mismatches between Pairs of Services. In:Computer Science and Information Technology (ICCSIT),2010 3rd IEEE International Conference on
[16]Liangming Li,Lei Liu,Zhijian Wang,Yelong Tang. Research on Interface Automata Testing. In:Computer Science and Software Engineering,2008 International Conference
[17]Linyuan Liu,Zhiqiu Huang,Fangxiong Xiao,Guohua Shen,Haibin Zhu. Verification of Privacy Requirements in Web Services Composition, in:Data, Privacy and E-Commerce (ISDPE),2010 Second International Symposium
[18]Jaideep Chandrashekar, Zhi-Li Zhang, Zhenhai Duan and Y. Thomas Hou. Service Oriented Internet. In:Lecture Notes in Computer Science,2003, Volume 2910/2003
[19]张佩云,黄波.基于Petri网的Web服务组合模型描述和验证.系统仿真学报,2007
[20]Kiam Tian Seow, Ming Gai, Tong Lee Lim. A Temporal Logic Specification Interface for Automata-Theoretic Finitary Control Synthesis. In:Proceedings of the 2005 IEEE International Conference on Robotics and Automation Barcelona, Spain, April 2005
[21]Samir Chouali, Sebti Mouelhi, Hassan Mountassir. Adapting Component Behaviours using Interface Automata. In:2010 36th EUROMICRO Conference on Software Engineering and Advanced Applications
[22]于守健,李卫民,吴国文,乐嘉锦.BPEL中基于有限状态自动机的Web服务自动组合.小型微型计算机系统,2007年4月第4期
[23]Yong-Lian Wang, Xue-Li Yu. Formalization and Verification of Automatic Composition Based on Pi-Calculus for Semantic Web Service. In:2009 Second International Symposium on Knowledge Acquisition and Modeling
[24]Ernesto Wandeler, J.W. Janneck, Edward A. Lee, Lothar Thiele. Counting Interface Automata and their Application. In:Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'2005)
[25]Zhe Chen, Gilles Motet. Formalizing Safety Requirements Using Controlling Automata. In:2009 Second International Conference on Dependability
[26]Sebastian Nanz, Terkel K. Tolstrup. Goal-oriented composition of services. In: Lecture Notes in Computer Science,2008, Volume 4954/2008,109-124,
[27]程锋涛.MWB的BPEL到π演算自动转换工具的研究与实现：[硕士学位论文].西安：西北大学,2010
[28]Xutao Du, Chunxiao Xing, Lizhu Zhou. Nested Web Service Interface Control Flow Automata. In:2008 4th International Conference on Next Generation Web Services Practices
[29]Zhang Jing-zhou, Ren Hong-min, GE Xiao-Kun, QIAN Le-Qiu,ZHU San-Yuan. Research on Component Behavior Protocols Mismatch Detection and Limited. In: 2009 10th ACIS International Conference on Software Engineering, Artificial Intelligences, Networking and Parallel/Distributed Computing
[30]徐丙凤,胡军,曹东,黄志球,郭丽娟,张剑.T-CBESD:一个构件化嵌入式软件设计模型验证工具.小型微型计算机系统,2010年11月第11期
[31]Zining Cao. Temporal Logics and Model Checking Algorithms for ZIAs. In: Software Engineering and Data Mining (SEDM),2010 2nd International Conference
[32]Haiqiang Dun, Haiying Xu, Lifu Wang. Transformation of BPEL Processes to Petri Nets. In:2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering
[33]李良明,王志坚,唐龙业.构件功能行为测试的研究,小型微型计算机系统,2010年4月第4期
[34]杨春霞,王映辉,王宏涛.构件组合的一致性验证和冗余行为去除,计算机工程,第36卷第24期
[35]廖军,谭浩,刘锦德.基于Pi演算的Web服务组合的描述和验证,计算机学报,2005年第28卷第4期
[36]胡军,于笑丰,张岩等.基于场景构件式实时软件设计的一致性检验,Journal of Software, Vol.17, No.1, January 2006, pp.48-58
[37]胡军,于笑丰,张岩,等.基于场景规约的构件式系统设计分析与验证,计算机学报,2006年第29卷第4期
[38]Henrique Jorge A. Holanda. a Framework for the Performance Analysis of Web Services Orchestrated with BPEL4WS.2009 fourth international conference on internet and web application and service[J].2009:363-369
[39]王晓燕,刘淑芬,于海.基于接口自动机的服务组合方法,吉林大学学报(工学版),2009年第39卷第3期
[40]邱剑锋,王申康,马勤勇,王玥,徐海长.描述逻辑在基于语义的服务消息交互中的应用, 计算机应用研究,2009,第26卷第1期
[41]胡军, 黄志球, 曹东等.网构软件的资源自适应性的形式化分析与验证,软件学报,2008,Vol.19,No5
[42]史忠植,常亮.基于动态描述逻辑的语义Web服务推理,计算机学报,2008,第31卷第9期
[43]谭亮,曾红卫.基于接口自动机的Web应用验证,计算机工程与应用,2009,45(3)
[44]邓水光.Web服务自动组合与形式化验证的研究：[博士学位论文].杭州：浙江大学,2007
[45]于守健.基于Web服务组合的业务流程集成关键技术研究：[博士学位论文].吉林：东北大学,2005
[46]文艳军.基于接口自动机的组合验证方法研究：[博士学位论文].长沙：国防科技大学,2005
[47]邱剑锋.基于语义的自动化服务组合研究：[硕士学位论文].杭州：浙江大学,2008
[48]Seyyed Vahid Hashemian, Farhad Mavaddat. A Graph-Based Approach to Web Services Composition. In:Proceedings of the 2005 Symposium on Applications and the Internet (SAINT'05)
[49]Shahram Esmaeilsabzali, Farhad Mavaddat, Nancy A.Day. Interface Automata with Complex Actions. In:Electronic Notes in Theoretical Computer Science 159 (2006) 79-97
[50]Philippe Balbiani, Fahima Cheikh, Guillaume Feuillade. Algorithms and Complexity of Automata Synthesis by Asynhcronous Orchestration With Applications to Web Services Composition. In:Electronic Notes in Theoretical Computer Science 229 (2009)3-18
[51]Samir Chouali, Hassan Mountassir, Sebti Mouelhi. An I/O Automata-based Approach to Verify Component Compatibility. In:Electronic Notes in Theoretical Computer Science 238 (2010) 3-13
[52]Hongyu Sun, Samik Basu, Robyn Lutz, Vasant Honavar. Automata-Based Verification of Non-Functional Requirements in Web service composition. In:Dept. of Computer Science Technical Report, Iowa State University,2009.
[53]Kun Gao, Lifeng Xi, Qin Wang. Binding Abstract Business Process and Actual Web Services Using Finite State Automata. In:2009 Fifth International Conference on Semantics, Knowledge and Grid
[54]Shahram Esmaeilsabzali, Nancy A. Day, Farhad Mavaddat. Interface Automata with Complex Actions:Limiting Interleaving in Interface Automata. In:Fundamenta Informaticae 82 (2008) 465-512
[55]Luca de Alfaro, Thomas A. Henzinger. Interface Automata. In:ACM SIGSOFT Software Engineering, Volume 26 Issue 5, Sept.2001
[56]Zhe Dang, Oscar H. Ibarra, Jianwen Su. On composition and lookahead delegation of e-services modeled by automata. Theoretical Computer Science 341 (2005) 344 363
[57]Sebti Mouelhi, Samir Chouali, Hassan Mountassir. Refinement of Interface Automata Strengthened by Action Semantics, Electronic Notes in Theoretical Computer Science 253 (2009) 111-126
[58]闻晓,张为群,杨阳,黄娟.BPEL应用程序验证模型研究[J].计算机科学,2009-4,36(4),page163-165
[59]严蔚敏,吴伟民编著.数据结构(C语言版).北京：清华大学出版社,2003,183-186
[60]Holzrnann G J. Software model checking with SPIN[J]. Journal of Advances in Computersm,2005.65:78-109
[61]UPPAAL. http://www.uppaal.com.2006-09-08
[62]Behrmann G, David A, Larsen K G, et al. UPPAAL 4.0[A].In:Proceedings of Third International Conference on the Quantitative Evaluation of Systems(QEST 2006)[c], IEEE Press,2006,125-126
[63]Adler B T, Alfaro L D, Silva LDD, et al. Ticc:a tool for interface compatibility and composition[R]. In:Technical Report ucsc-crl-06-01, School of Engineering, University of California, Santa Cruz.2006
[64]Alfaro LD, Silva L D D, Faella M, et al. Sociable interfaces[A]. In FROCOS 2005: 5th International Workshop on Frontiers of Combining Systems[C]. Berlin: Springer-Verlag, LNCS 3717,2005,81-105
[65]Ptolemy[EB/OL]. http://ptolemy.eccs.berkeley.edu/ptolemy-Ⅱ/.2008-02-07
[66]Cheng C P, Fristoe T. Lee E A. Applied verification:the ptolemy approach[R]. In: Technical Report UCB/EECS-2008-41. EECS Department, University of California, Berkeley,2008
[67]Heam, P.-C., Kouchnarenko O., Voinot, J. How to Handle QoS Aspects in Web Services Substitutivity Verification. In:Enabling Technologies:Infrastructure for Collaborative Enterprises,2007. WETICE 2007.16th IEEE International Workshops
[68]龚玲,张云涛译.Web服务原理和技术.机械工业出版社,2010,23-25
[69]蒋运承,史忠植.QoS驱动的主体服务匹配.小型微型计算机系统.2005,26(4)：687-692
[70]Hongbo Tian, Xiaoshe Dong, Xiaoyi Zhao, Lingping Zeng, Xingjun Zhang. A Novel SLA-driven Verification and Planning Framework for QoS. In:Information Management and Engineering (ICIME),2010 The 2nd IEEE International Conference
[71]Mallet F, Peraldi-Frati M.-A, Andre C. From UML to Petri Nets for non functional Property Verification. In:Industrial Embedded Systems,2006. IES '06. International Symposium
[2]Michael P. Papazoglou, Paolo Traverso, Schahran Dustdar, et al. Service-Oriented Computing:State of the Art and Research Challenges. Computer,2007,40(11):38-45
[3]M.P.Papazoglou, D.Georgakopoulous. Service-Oriented Computing. Communication of the ACM,2003,46(10):25-28
[4]SOAP Specifications.http://www.w3.org/TR/soap
[5]Web Services Description Language. http://www.w3.org/TR/wsdl
[6]Andrews T, Curbera F, et al. Business Process Execution Language for Web Servic e (BPEL4WS) 1.1,2003. http://www.ibm.com/developerworks/library/ws-bpel/.
[7]Resource Description Framework. http://www.w3.org/RDF/
[8]OWL Web Ontology Language Guide.http://www.w3.org/TR/2004/REC-owl-guide-20040210
[9]雷丽晖,段振华.一种基于扩展有限自动机验证组合Web服务的方法,Journal of Software, Vol.18, No.12, December 2007
[10]王晨,王红兵,许迅.一种验证Web服务流程的新方法,计算机应用研究,2008,第25卷第12期
[11]苏焕程,黄志球,刘林源.基于接口自动机的BPEL4WS+Web服务组合形式化模型,计算机应用研究,2009年第5期
[12]D Chenthati, S Vaddi, H Mohanty. Verification of Web Services Modeled as Finite State Machines. In:2010 Fourth Asia International Conference on Mathematical/Analytical Modelling and Computer Simulation
[13]Tao Liu, Guosun Zeng, Adaptation of Mismatching Services Based on Labelled Interface Automata. In:2009 Fifth International Conference on Semantics, Knowledge and Grid
[14]Tevfik Bultan,Xiang Fu,Richard Hull,Jianwen Su. An Interface Automata based Model for Web Service Composition. In:12th international conference on World Wide Web ACM New York, NY, USA 2003
[15]Tao Liu,Guosun Zeng. Detecting and Resolving Mismatches between Pairs of Services. In:Computer Science and Information Technology (ICCSIT),2010 3rd IEEE International Conference on
[16]Liangming Li,Lei Liu,Zhijian Wang,Yelong Tang. Research on Interface Automata Testing. In:Computer Science and Software Engineering,2008 International Conference
[17]Linyuan Liu,Zhiqiu Huang,Fangxiong Xiao,Guohua Shen,Haibin Zhu. Verification of Privacy Requirements in Web Services Composition, in:Data, Privacy and E-Commerce (ISDPE),2010 Second International Symposium
[18]Jaideep Chandrashekar, Zhi-Li Zhang, Zhenhai Duan and Y. Thomas Hou. Service Oriented Internet. In:Lecture Notes in Computer Science,2003, Volume 2910/2003
[19]张佩云,黄波.基于Petri网的Web服务组合模型描述和验证.系统仿真学报,2007
[20]Kiam Tian Seow, Ming Gai, Tong Lee Lim. A Temporal Logic Specification Interface for Automata-Theoretic Finitary Control Synthesis. In:Proceedings of the 2005 IEEE International Conference on Robotics and Automation Barcelona, Spain, April 2005
[21]Samir Chouali, Sebti Mouelhi, Hassan Mountassir. Adapting Component Behaviours using Interface Automata. In:2010 36th EUROMICRO Conference on Software Engineering and Advanced Applications
[22]于守健,李卫民,吴国文,乐嘉锦.BPEL中基于有限状态自动机的Web服务自动组合.小型微型计算机系统,2007年4月第4期
[23]Yong-Lian Wang, Xue-Li Yu. Formalization and Verification of Automatic Composition Based on Pi-Calculus for Semantic Web Service. In:2009 Second International Symposium on Knowledge Acquisition and Modeling
[24]Ernesto Wandeler, J.W. Janneck, Edward A. Lee, Lothar Thiele. Counting Interface Automata and their Application. In:Proceedings of the Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'2005)
[25]Zhe Chen, Gilles Motet. Formalizing Safety Requirements Using Controlling Automata. In:2009 Second International Conference on Dependability
[26]Sebastian Nanz, Terkel K. Tolstrup. Goal-oriented composition of services. In: Lecture Notes in Computer Science,2008, Volume 4954/2008,109-124,
[27]程锋涛.MWB的BPEL到π演算自动转换工具的研究与实现：[硕士学位论文].西安：西北大学,2010
[28]Xutao Du, Chunxiao Xing, Lizhu Zhou. Nested Web Service Interface Control Flow Automata. In:2008 4th International Conference on Next Generation Web Services Practices
[29]Zhang Jing-zhou, Ren Hong-min, GE Xiao-Kun, QIAN Le-Qiu,ZHU San-Yuan. Research on Component Behavior Protocols Mismatch Detection and Limited. In: 2009 10th ACIS International Conference on Software Engineering, Artificial Intelligences, Networking and Parallel/Distributed Computing
[30]徐丙凤,胡军,曹东,黄志球,郭丽娟,张剑.T-CBESD:一个构件化嵌入式软件设计模型验证工具.小型微型计算机系统,2010年11月第11期
[31]Zining Cao. Temporal Logics and Model Checking Algorithms for ZIAs. In: Software Engineering and Data Mining (SEDM),2010 2nd International Conference
[32]Haiqiang Dun, Haiying Xu, Lifu Wang. Transformation of BPEL Processes to Petri Nets. In:2008 2nd IFIP/IEEE International Symposium on Theoretical Aspects of Software Engineering
[33]李良明,王志坚,唐龙业.构件功能行为测试的研究,小型微型计算机系统,2010年4月第4期
[34]杨春霞,王映辉,王宏涛.构件组合的一致性验证和冗余行为去除,计算机工程,第36卷第24期
[35]廖军,谭浩,刘锦德.基于Pi演算的Web服务组合的描述和验证,计算机学报,2005年第28卷第4期
[36]胡军,于笑丰,张岩等.基于场景构件式实时软件设计的一致性检验,Journal of Software, Vol.17, No.1, January 2006, pp.48-58
[37]胡军,于笑丰,张岩,等.基于场景规约的构件式系统设计分析与验证,计算机学报,2006年第29卷第4期
[38]Henrique Jorge A. Holanda. a Framework for the Performance Analysis of Web Services Orchestrated with BPEL4WS.2009 fourth international conference on internet and web application and service[J].2009:363-369
[39]王晓燕,刘淑芬,于海.基于接口自动机的服务组合方法,吉林大学学报(工学版),2009年第39卷第3期
[40]邱剑锋,王申康,马勤勇,王玥,徐海长.描述逻辑在基于语义的服务消息交互中的应用, 计算机应用研究,2009,第26卷第1期
[41]胡军, 黄志球, 曹东等.网构软件的资源自适应性的形式化分析与验证,软件学报,2008,Vol.19,No5
[42]史忠植,常亮.基于动态描述逻辑的语义Web服务推理,计算机学报,2008,第31卷第9期
[43]谭亮,曾红卫.基于接口自动机的Web应用验证,计算机工程与应用,2009,45(3)
[44]邓水光.Web服务自动组合与形式化验证的研究：[博士学位论文].杭州：浙江大学,2007
[45]于守健.基于Web服务组合的业务流程集成关键技术研究：[博士学位论文].吉林：东北大学,2005
[46]文艳军.基于接口自动机的组合验证方法研究：[博士学位论文].长沙：国防科技大学,2005
[47]邱剑锋.基于语义的自动化服务组合研究：[硕士学位论文].杭州：浙江大学,2008
[48]Seyyed Vahid Hashemian, Farhad Mavaddat. A Graph-Based Approach to Web Services Composition. In:Proceedings of the 2005 Symposium on Applications and the Internet (SAINT'05)
[49]Shahram Esmaeilsabzali, Farhad Mavaddat, Nancy A.Day. Interface Automata with Complex Actions. In:Electronic Notes in Theoretical Computer Science 159 (2006) 79-97
[50]Philippe Balbiani, Fahima Cheikh, Guillaume Feuillade. Algorithms and Complexity of Automata Synthesis by Asynhcronous Orchestration With Applications to Web Services Composition. In:Electronic Notes in Theoretical Computer Science 229 (2009)3-18
[51]Samir Chouali, Hassan Mountassir, Sebti Mouelhi. An I/O Automata-based Approach to Verify Component Compatibility. In:Electronic Notes in Theoretical Computer Science 238 (2010) 3-13
[52]Hongyu Sun, Samik Basu, Robyn Lutz, Vasant Honavar. Automata-Based Verification of Non-Functional Requirements in Web service composition. In:Dept. of Computer Science Technical Report, Iowa State University,2009.
[53]Kun Gao, Lifeng Xi, Qin Wang. Binding Abstract Business Process and Actual Web Services Using Finite State Automata. In:2009 Fifth International Conference on Semantics, Knowledge and Grid
[54]Shahram Esmaeilsabzali, Nancy A. Day, Farhad Mavaddat. Interface Automata with Complex Actions:Limiting Interleaving in Interface Automata. In:Fundamenta Informaticae 82 (2008) 465-512
[55]Luca de Alfaro, Thomas A. Henzinger. Interface Automata. In:ACM SIGSOFT Software Engineering, Volume 26 Issue 5, Sept.2001
[56]Zhe Dang, Oscar H. Ibarra, Jianwen Su. On composition and lookahead delegation of e-services modeled by automata. Theoretical Computer Science 341 (2005) 344 363
[57]Sebti Mouelhi, Samir Chouali, Hassan Mountassir. Refinement of Interface Automata Strengthened by Action Semantics, Electronic Notes in Theoretical Computer Science 253 (2009) 111-126
[58]闻晓,张为群,杨阳,黄娟.BPEL应用程序验证模型研究[J].计算机科学,2009-4,36(4),page163-165
[59]严蔚敏,吴伟民编著.数据结构(C语言版).北京：清华大学出版社,2003,183-186
[60]Holzrnann G J. Software model checking with SPIN[J]. Journal of Advances in Computersm,2005.65:78-109
[61]UPPAAL. http://www.uppaal.com.2006-09-08
[62]Behrmann G, David A, Larsen K G, et al. UPPAAL 4.0[A].In:Proceedings of Third International Conference on the Quantitative Evaluation of Systems(QEST 2006)[c], IEEE Press,2006,125-126
[63]Adler B T, Alfaro L D, Silva LDD, et al. Ticc:a tool for interface compatibility and composition[R]. In:Technical Report ucsc-crl-06-01, School of Engineering, University of California, Santa Cruz.2006
[64]Alfaro LD, Silva L D D, Faella M, et al. Sociable interfaces[A]. In FROCOS 2005: 5th International Workshop on Frontiers of Combining Systems[C]. Berlin: Springer-Verlag, LNCS 3717,2005,81-105
[65]Ptolemy[EB/OL]. http://ptolemy.eccs.berkeley.edu/ptolemy-Ⅱ/.2008-02-07
[66]Cheng C P, Fristoe T. Lee E A. Applied verification:the ptolemy approach[R]. In: Technical Report UCB/EECS-2008-41. EECS Department, University of California, Berkeley,2008
[67]Heam, P.-C., Kouchnarenko O., Voinot, J. How to Handle QoS Aspects in Web Services Substitutivity Verification. In:Enabling Technologies:Infrastructure for Collaborative Enterprises,2007. WETICE 2007.16th IEEE International Workshops
[68]龚玲,张云涛译.Web服务原理和技术.机械工业出版社,2010,23-25
[69]蒋运承,史忠植.QoS驱动的主体服务匹配.小型微型计算机系统.2005,26(4)：687-692
[70]Hongbo Tian, Xiaoshe Dong, Xiaoyi Zhao, Lingping Zeng, Xingjun Zhang. A Novel SLA-driven Verification and Planning Framework for QoS. In:Information Management and Engineering (ICIME),2010 The 2nd IEEE International Conference
[71]Mallet F, Peraldi-Frati M.-A, Andre C. From UML to Petri Nets for non functional Property Verification. In:Industrial Embedded Systems,2006. IES '06. International Symposium