| Web服务编制的形式化模型研究 |
| |
| 引用本文： | 杨晓波.Web服务编制的形式化模型研究[J].计算机工程,2012,38(7):276-278. |
| |
| 作者姓名： | 杨晓波 |
| |
| 作者单位： | 浙江财经学院东方学院信息分院,杭州,310018 |
| |
| 基金项目： | 浙江省自然科学基金资助项目(Y1110023) |
| |
| 摘 要： | 为支持对业务流程执行语言(BPEL)语言的形式化分析和验证，提出一种Web服务编制的形式化模型——μ-BPEL。介绍模型的语法规则和操作语义，在此基础上，建立从μ-BPEL到扩展时间自动机的映射，利用模型检查技术研究服务正确性检验和与时间相关的检验问题。研究结果表明，该模型符合Web服务编制流程，满足系统设定的时态逻辑性质。
|
| 关 键 词： | Web服务编制 形式化模型 时间自动机 映射 |
| 收稿时间： | 2011-07-04 |
Research on Formalization Model for Web Service Compilation |
| |
| YANG Xiao-bo.Research on Formalization Model for Web Service Compilation[J].Computer Engineering,2012,38(7):276-278. |
| |
| Authors: | YANG Xiao-bo |
| |
| Affiliation: | YANG Xiao-bo(Information School,Oriental College,Zhejiang University of Finance & Economics,Hangzhou 310018,China) |
| |
| 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. |
| |
| Keywords: | Web service compilation formalization model timed automata mapping |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
| 点击此处可从《计算机工程》浏览原始摘要信息 |
|
点击此处可从《计算机工程》下载全文 |
|
