为支持对业务流程执行语言(BPEL)语言的形式化分析和验证,提出一种Web服务编制的形式化模型——μ-BPEL.介绍模型的语法规则和操作语义,在此基础上,建立从μ-BPEL到扩展时间自动机的映射,利用模型检查技术研究服务正确性检验和与时间相关的检验问题.研究结果表明,该模型符合Web服务编制流程,满足系统设定的时态逻辑性质.%In order to support the formalization analysis and verification of Web Services-business Process Execution Language(BPEL), aformalization model for Web service compilation-μ-BPEL is designed in this paper. The specific studying process is as follows. The syntax rulesand operational semantics of u-BPEL language are introduced, and establishes the mapping from u-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.
展开▼
