Web服务编制的形式化模型研究  

Research on Formalization Model for Web Service Compilation

作　　者：杨晓波[1] 

机构地区：[1]浙江财经学院东方学院信息分院,杭州310018

出　　处：《计算机工程》2012年第7期276-278,共3页Computer Engineering

基　　金：浙江省自然科学基金资助项目(Y1110023)

摘　　要：为支持对业务流程执行语言(BPEL)语言的形式化分析和验证,提出一种Web服务编制的形式化模型——μ-BPEL。介绍模型的语法规则和操作语义,在此基础上,建立从μ-BPEL到扩展时间自动机的映射,利用模型检查技术研究服务正确性检验和与时间相关的检验问题。研究结果表明,该模型符合Web服务编制流程,满足系统设定的时态逻辑性质。In order to support the formalization analysis and verification of Web Services-business Process Execution Language（BPEL）,a formalization model for Web service compilation——μ-BPEL is designed in this paper.The specific studying process is as follows.The syntax rules and operational semantics of μ-BPEL language are introduced,and establishes the mapping from μ-BPEL to extended timed automata,model checking technology is used to study the service correctness and the test of time-related problems.Research result shows this model can support Web service compilation process effectively,which can better meet the temporal logical properties which sets in the system.

关 键 词：Web服务编制 形式化模型 时间自动机 映射 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]