| 基于Alloy的服务组合验证 |
| |
| 引用本文： | 曹玖新,吴江林,王国进,刘 波,杨鹏伟,董 丹. 基于Alloy的服务组合验证[J]. 通信学报, 2012, 33(Z2): 1-8. DOI: 10.3969/j.issn.1000-436x.2012.z2.001 |
| |
| 作者姓名： | 曹玖新 吴江林 王国进 刘 波 杨鹏伟 董 丹 |
| |
| 摘 要： | 服务组合是服务计算的核心问题，而服务组合的正确性与可算性则是服务正确执行的前提保证。首先提出一种基于Alloy的服务组合验证方法，采用有限的状态机建模WS-BPEL业务流程的状态变迁，利用Alloy语言对待验证的属性进行描述，通过Alloy模型完成有限状态机的形式化，最后使用Alloy Analyzer分析组合服务是否满足验证属性要求。实验研究表明，所提出的基于Alloy的服务组合验证方法具有较好的可行性。
|
Alloy-based verification of Web service composition |
| |
| Jiu-xin CAO,Jiang-lin WU,Guo-jin WANG,Bo LIU,Peng-wei YANG,Dan DONG. Alloy-based verification of Web service composition[J]. Journal on Communications, 2012, 33(Z2): 1-8. DOI: 10.3969/j.issn.1000-436x.2012.z2.001 |
| |
| Authors: | Jiu-xin CAO Jiang-lin WU Guo-jin WANG Bo LIU Peng-wei YANG Dan DONG |
| |
| Affiliation: | 1. School of Computer Science and Engineering,Southeast University,Nanjing 210096,China;2. Key Laboratory of Computer Network and Information Integration,Ministry of Education,Southeast University,Nanjing 210096,China;3. Huawei Technologies Co.,Nanjing 210012,China |
| |
| Abstract: | Service composition was the core problem of service computing,the validity and reliability of service composition had become the premise of service execution.A method was presented which utilizes the finite state machine (FSM)to model the business process’s state transitions,and described the required properties with Alloy language.Then,Alloy model was used to formalize the service FSM and the required properties of the system.Finally,Alloy Analyzer was used to verify the model that whether the required properties were satisfied.It is shown that the method of Alloy-based verification of the service composition is of good feasibility. |
| |
| Keywords: | Web service service composition finite state machine Alloy verification |
|
| 点击此处可从《通信学报》浏览原始摘要信息 |
|
点击此处可从《通信学报》下载全文 |
|
