时间约束条件下Web服务组合的形式化分析与验证  

Formal Analysis and Verification of Web Service Compositions with Timing Constraints

作　　者：陈志辉[1] 吴敏敏[1] 

机构地区：[1]莆田学院信息工程学院,福建莆田351100

出　　处：《贵州大学学报（自然科学版）》2015年第5期69-75,共7页Journal of Guizhou University:Natural Sciences

基　　金：福建省中青年教师教育科研项目(A类)(JA14279);莆田市科技项目(2014G16);莆田学院教育教学改革研究项目(JG2012006)资助

摘　　要：随着Web技术和商业应用的快速发展,Web服务组合技术已成构建电子商务应用的主要方法之一。当前,为适应快速变化的商业环境,对商业应用提出了实时性的要求,即限定服务的行为必须满足给定的时间约束条件。文中提出了一种形式化方法,用于分析与验证Web服务组合的时间约束行为。首先,扩展了Web服务接口描述语言,增加对时间约束的描述,然后定义一种时间行为自动机,用于刻画Web服务组合的时间行为,最终利用模型验证技术来自动验证这些行为是否满足给定的时间属性。通过对股票分析应用场景以及使用UPPAAL模型验证工具,表明该方法的可行性和有效性。With the rapid development of Web technology and commercial application, Web service composition technology has become one of the main methods for building electronic commerce applications. At present, In or- der to adapt to the fast-changing business environment, People put forward the requirements of real-time for com- mercial applications at present. A formal method was presented for analyzing and verifying time-related properties of Web service compositions. We extend web service interface with timing requirements, then introduce formal- ism, called Timed Behavior Automata, to capture timed behavior of web services, and verify the behavior proper- ties of composite web services by using model-checking techniques. The case study in a model checker UPPAAL shows that our method is feasible and effective.

关 键 词：服务组合 形式化方法 时间自动机 UPPAAL 模型检查 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]