English

应用科学学报 ›› 2010, Vol. 28 ›› Issue (3): 326-330.

• 计算机科学与应用 • 上一篇    

OWL-S到Z规格说明的转换

王毅俊1;2， 缪淮扣1;2， 许庆国1， 曹晓夏1   

  1. 1．上海大学计算机工程与科学学院，上海200072
    2．上海市计算机软件评测重点实验室，上海201112
  • 收稿日期:2009-08-03 修回日期:2009-12-30 出版日期:2010-05-21 发布日期:2010-05-21
  • 作者简介:缪淮扣，教授，博导，研究方向：软件形式方法，E-mail：hkmiao@shu.edu.cn
  • 基金资助:

    国家“973”重大基础研究发展计划基金(No.2007CB310800)； 国家“863”高技术研究发展计划基金(No.2007AA01Z144)；国家自然科学基金(No.60673115, No.60970007)； 上海市自然科学基金(No.09ZR1412100)； 上海市重点学科建设项目基金(No.J50103)资助

Transformation from OWL-S Model to Z

WANG Yi-jun1;2, MIAO Huai-kou1;2, XU Qing-guo1, CAO Xiao-xia1   

  1. 1. School of Computer Engineering and Science, Shanghai University, Shanghai 200072, China
    2. Shanghai Key Laboratory of Computer Software Testing and Evaluating, Shanghai 201112, China
  • Received:2009-08-03 Revised:2009-12-30 Online:2010-05-21 Published:2010-05-21

PDF

1875

摘要：

OWL-S是重要的Semantic Web Service描述框架，但缺乏有效的形式化验证工具. Z语言是基于集合论和一阶谓词逻辑的形式化规格说明语言，比OWL-S具有更强的表达力. 该文研究基于Z的OWL-S形式化方法，提出从OWL-S到Z规格说明的模型转换规则. 基于这些规则，用Z定义OWL-S中概念的形式化语义，并开发了从OWL-S描述到Z规格说明的自动转换工具OWLS2Z.

关键词: 语义网络服务, OWL-S, Z规格说明, 形式方法, 转换规则

Abstract:

OWL-S is one of the most significant Semantic Web Service frameworks, but is short of effective formal verification tools. Z is a formal specification language based upon set theory and mathematical logic that is more expressive than OWL-S. This paper studies the formal method for OWL-S based on Z. A set of model transforming rules is proposed. The semantics of OWL-S concepts are defined using Z based on these rules. A tool prototype (OWLS2Z) transforming OWL-S model to Z is presented.

Key words: Semantic Web Service, OWL-S, the Z notation, formal method, transforming rules

中图分类号: