Towards the formal model and verification of web service choreography description language

被引：0
|
作者：
Zhao Xiangpeng [1 ]
Yang Hongli
Qiu Zongyan
机构：
[1] Peking Univ, Sch Math, LMAM, Beijing 100871, Peoples R China
[2] Peking Univ, Sch Math, Dept Informat, Beijing 100871, Peoples R China
来源：
WEB SERVICES AND FORMAL METHODS, PROCEEDINGS | 2006年 / 4184卷
关键词：
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
The Web Services Choreography Description Language (WS-CDL) is a W3C specification for the description of peer-to-peer collaborations of participants from a global viewpoint. For the rigorous development and tools support for the language, the formal semantics of WS-CDL is worth investigating. This paper proposes a small language CDL as a formal model of the simplified WS-CDL, which includes important concepts related to participant roles and collaborations among them in a choreography. The formal operational semantics of CDL is given. Based on the formal model, we discuss further: 1) project a given choreography to orchestration views, which provides a basis for the implementation of the choreography by code generation; 2) translate WS-CDL to the input language of the model-checker SPIN, which allows us to automatically verify the correctness of a given choreography. An automatic translator has been implemented.
引用
收藏
页码：273 / 287
页数：15
相关论文
共 50 条
  • [1] A formal model for Web Service Choreography Description Language (WS-CDL)
    Yang, Hongli
    Zhao, Xiangpeng
    Qiu, Zongyan
    Pu, Geguang
    Wang, Shuling
    [J]. ICWS 2006: IEEE INTERNATIONAL CONFERENCE ON WEB SERVICES, PROCEEDINGS, 2006, : 893 - +
  • [2] Towards the semantics for web service choreography description language
    Li, Jing
    He, Jifeng
    Pu, Geguang
    Zhu, Huibiao
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2006, 4260 : 246 - +
  • [3] A Formal Method for Service Choreography Verification Based on Description Logic
    Zhang, Tingting
    Lan, Yushi
    Yu, Minggang
    Zheng, Changyou
    Liu, Kun
    [J]. CMC-COMPUTERS MATERIALS & CONTINUA, 2020, 62 (02): : 893 - 904
  • [4] Web Service Choreography Verification Using Z Formal Specification
    Rastegari, Y.
    Sajadi, Z.
    Shams, F.
    [J]. INTERNATIONAL JOURNAL OF ENGINEERING, 2016, 29 (11): : 1549 - 1557
  • [5] Towards formal verification of web service composition
    Bai, XX
    Fan, YS
    [J]. PROCEEDINGS OF THE 11TH INTERNATIONAL CONFERENCE ON INDUSTRIAL ENGINEERING AND ENGINEERING MANAGEMENT, VOLS 1 AND 2: INDUSTRIAL ENGINEERING AND ENGINEERING MANAGEMENT IN THE GLOBAL ECONOMY, 2005, : 577 - 581
  • [6] Towards formal verification of web service composition
    Rouached, Mohsen
    Perrin, Olivier
    Godart, Claude
    [J]. BUSINESS PROCESS MANAGEMENT, PROCEEDINGS, 2006, 4102 : 257 - 273
  • [7] Compatibility verification for web service choreography
    Foster, H
    Uchitel, S
    Magee, J
    Kramer, J
    [J]. IEEE INTERNATIONAL CONFERENCE ON WEB SERVICES, PROCEEDINGS, 2004, : 738 - 741
  • [8] Formal description and verification of Web service composition based on OOPN
    Su, Jindian
    Yu, Shanshan
    Guo, Heqing
    [J]. ADVANCED INTELLIGENT COMPUTING THEORIES AND APPLICATIONS, PROCEEDINGS: WITH ASPECTS OF THEORETICAL AND METHODOLOGICAL ISSUES, 2008, 5226 : 644 - +
  • [9] A Logical Representation and Verification of Web Service Choreography
    Madani, Zahra
    Nematbakhsh, Naser
    Zamanifar, Kamran
    Mardukhi, Frahad
    [J]. 2009 THIRD INTERNATIONAL SYMPOSIUM ON INTELLIGENT INFORMATION TECHNOLOGY APPLICATION, VOL 2, PROCEEDINGS, 2009, : 404 - +
  • [10] WEB SERVICE CHOREOGRAPHY CONFORMANCE VERIFICATION THROUGH THE piX-MODEL
    Van Seghbroeck, Gregory
    Volckaert, Bruno
    De Turck, Filip
    Dhoedt, Bart
    Demeester, Piet
    [J]. INTERNATIONAL JOURNAL OF COOPERATIVE INFORMATION SYSTEMS, 2010, 19 (1-2) : 1 - 30
12345