摘要： 为支持对业务流程执行语言(BPEL)语言的形式化分析和验证，提出一种Web服务编制的形式化模型——μ-BPEL。介绍模型的语法规则和操作语义，在此基础上，建立从μ-BPEL到扩展时间自动机的映射，利用模型检查技术研究服务正确性检验和与时间相关的检验问题。研究结果表明，该模型符合Web服务编制流程，满足系统设定的时态逻辑性质。

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

Abstract: 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.

Key words: Web service compilation, formalization model, timed automata, mapping

中图分类号: 

• TP391