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 条
  • [31] REFINER: Towards Formal Verification of Model Transformations
    Wijs, Anton
    Engelen, Luc
    [J]. NASA FORMAL METHODS, NFM 2014, 2014, 8430 : 258 - 263
  • [32] Towards a Formal Model of Language Networks
    Kirigin, Tajana Ban
    Mestrovic, Ana
    Martincic-Ipsic, Sanda
    [J]. INFORMATION AND SOFTWARE TECHNOLOGIES, ICIST 2015, 2015, 538 : 469 - 479
  • [33] The semantics and verification of timed service choreography
    Zhao, Yongxin
    Xiao, Hao
    Wang, Zheng
    Pu, Geguang
    Su, Ting
    [J]. INTERNATIONAL JOURNAL OF COMPUTER MATHEMATICS, 2014, 91 (03) : 384 - 402
  • [34] A FRAMEWORK FOR MODEL CHECKING WEB SERVICE CHOREOGRAPHY BASED ON CWB
    Beggar, Mohammed Lamine
    Liao Lejian
    [J]. 2011 3RD INTERNATIONAL CONFERENCE ON COMPUTER TECHNOLOGY AND DEVELOPMENT (ICCTD 2011), VOL 3, 2012, : 497 - 507
  • [35] Web service choreography model based on concurrent transaction logic
    Wang, Yong
    Jiang, Zheng-Tao
    Hou, Ya-Rong
    Fang, Juan
    Mao, Guo-Jun
    [J]. Beijing Gongye Daxue Xuebao / Journal of Beijing University of Technology, 2009, 35 (08): : 1132 - 1137
  • [36] A formal description framework and a matchmaking technique for web service composition
    Karunamurthy, Rajesh
    Khendek, Ferhat
    Glitho, Roch H.
    [J]. INTERNATIONAL JOURNAL OF WEB INFORMATION SYSTEMS, 2010, 6 (01) : 24 - +
  • [37] Type checking choreography description language
    Yang, Hongli
    Zhao, Xiangpeng
    Qiu, Zongyan
    Cai, Chao
    Pu, Geguang
    [J]. Formal Methods and Software Engineering, Proceedings, 2006, 4260 : 264 - 283
  • [38] A New Description Model of Web Service
    Wu, Shaofei
    [J]. 2009 INTERNATIONAL CONFERENCE ON INDUSTRIAL AND INFORMATION SYSTEMS, PROCEEDINGS, 2009, : 77 - 79
  • [39] A formal model for semantic Web service composition
    Lecue, Freddy
    Leger, Alain
    [J]. SEMANTIC WEB - ISEC 2006, PROCEEDINGS, 2006, 4273 : 385 - 398
  • [40] A QoS view of web service choreography
    Zhao Xiangpeng
    Cai Chao
    Yang Hongli
    Qiu Zongyan
    [J]. ICEBE 2007: IEEE INTERNATIONAL CONFERENCE ON E-BUSINESS ENGINEERING, PROCEEDINGS, 2007, : 607 - +
12345