...
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of network and computer applications >Model-driven approach supporting formal verification for web service composition protocols
【24h】

Model-driven approach supporting formal verification for web service composition protocols

机译：模型驱动的方法支持对Web服务组合协议的形式验证

获取原文
获取原文并翻译 | 示例
           
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

Composite Web services development is a complex task involving specification, verification, implementation, and testing. Despite the fact that several languages have been proposed for composing Web services (e.g., BPEL, WSCI), there is a lack of well-defined formal semantics for formal analysis and verification. Moreover, current approaches are specific to a given programming language (e.g. BPEL) and they focus only on the verification of already implemented composite services. This paper proposes an approach for specifying, verifying and implementing composite services according to the Model-Driven Architecture principles. It makes use of formal methods, especially the LOTOS formal description language, to support composition verification at specification time. The benefit is that the composition specification is proven to be correct before its implementation with a programming language such as BPEL. A case study is also presented to show how a service composition can be specified in a workflow and then formally verified before executable code generation.
机译：组合Web服务开发是一项复杂的任务，涉及规范，验证，实现和测试。尽管已经提出了几种用于组成Web服务的语言（例如BPEL，WSCI），但仍缺乏用于形式分析和验证的定义明确的形式语义。而且，当前的方法专用于给定的编程语言（例如BPEL），并且它们仅关注于已经实施的组合服务的验证。本文提出了一种根据模型驱动体系结构原则指定，验证和实现组合服务的方法。它利用形式化方法，尤其是LOTOS形式化描述语言，来支持规范时的成分验​​证。这样做的好处是，在使用诸如BPEL之类的编程语言实现合成规范之前，事实证明合成规范是正确的。还提供了一个案例研究，以说明如何在工作流中指定服务组合，然后在生成可执行代码之前对其进行正式验证。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号